awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
have obtain : ∀ (b : A) (hb : orderOf b = n) (hab : a ∈ ball b δ), (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
Tactic: obtain ⟨b, hb, hab⟩ := mem_approxOrderOf_iff.mp ha
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
have rw : ∀ (hmn : (orderOf b).Coprime m) (hb : orderOf b = n) (hab : a ∈ ball b δ),
  Membership.mem (γ := Set A) {u : A | orderOf u = orderOf b} (b ^ m)
Tactic: rw [← hb] at hmn ⊢
Cleared hypotheses: hmn, hb, hab
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
have hb₁ : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
Tactic: replace hb : b ^ m ∈ {u : A | orderOf u = n} := by
    rw [← hb] at hmn ⊢; exact hmn.orderOf_pow
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
have a₁ : (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ)
Tactic: apply ball_subset_thickening hb ((m : ℝ) • δ)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
⊢ (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ)
have h : ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ) = ball (b ^ m) (m • δ)
Tactic: convert! pow_mem_ball hm hab using 1
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
have obtain : ∀ (b : A) (hb : orderOf b = n * m) (hab : a ∈ ball b δ), (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
Tactic: obtain ⟨b, hb : orderOf b = n * m, hab : a ∈ ball b δ⟩ := mem_approxOrderOf_iff.mp ha
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
have rw : orderOf (b ^ m) = n
Tactic: rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
rw : orderOf (b ^ m) = n
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
have rw₁ : orderOf b / (orderOf b).gcd m = n
Tactic: rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
rw : orderOf (b ^ m) = n
rw₁ : orderOf b / (orderOf b).gcd m = n
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
have rw₂ : n * m / (n * m).gcd m = n
Tactic: rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
rw : orderOf (b ^ m) = n
rw₁ : orderOf b / (orderOf b).gcd m = n
rw₂ : n * m / (n * m).gcd m = n
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
have rw₃ : n * m / m = n
Tactic: rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
rw : orderOf (b ^ m) = n
rw₁ : orderOf b / (orderOf b).gcd m = n
rw₂ : n * m / (n * m).gcd m = n
rw₃ : n * m / m = n
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
have rw₄ : n = n
Tactic: rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
have hb₁ : Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
Tactic: replace hb : b ^ m ∈ {y : A | orderOf y = n} := by
    rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
have a₁ : (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) ((↑m : ℝ) * δ)
Tactic: apply ball_subset_thickening hb (m * δ)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
⊢ (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) ((↑m : ℝ) * δ)
have h : ball (b ^ m) ((↑m : ℝ) * δ) = ball (b ^ m) (m • δ)
Tactic: convert! pow_mem_ball hm hab using 1
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ
have simp_rw : Subset.{u_1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
  (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ)
Tactic: simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ Subset.{u_1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ)
have refine : ∀ (b : A) (hb : orderOf b = n) (c : A) (hc : c ∈ ball (a * b) δ),
  Membership.mem (γ := Set A) (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ) c
Tactic: refine iUnion₂_subset_iff.mpr fun b hb c hc => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ Membership.mem (γ := Set A) (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ) c
have simp : ∃ (i : A), orderOf i = orderOf a * n ∧ c ∈ ball i δ
Tactic: simp only [mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ ∃ (i : A), orderOf i = orderOf a * n ∧ c ∈ ball i δ
have refine : orderOf (a * b) = orderOf a * n
Tactic: refine ⟨a * b, ?_, hc⟩
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ orderOf (a * b) = orderOf a * n
have rw : ∀ (han : (orderOf a).Coprime (orderOf b)) (hb : orderOf b = n) (c : A) (hc : c ∈ ball (a * b) δ),
  orderOf (a * b) = orderOf a * orderOf b
Tactic: rw [← hb] at han ⊢
Cleared hypotheses: han, hb, c, hc
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ n
⊢ a • approxOrderOf A n δ = approxOrderOf A n δ
have simp_rw : Eq.{u_1 + 1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
  (⋃ (x : A), ⋃ (_ : orderOf x = n), ball x δ)
Tactic: simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ n
b : A
hb : orderOf b = n
⊢ orderOf (a * b) = n
have hn₁ : 0 < orderOf b
Tactic: rw [← hb] at han hn
Cleared hypotheses: hn, han, hb
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ n
b : A
hb : orderOf b = n
hn₁ : 0 < orderOf b
⊢ orderOf (a * b) = n
have han₁ : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ orderOf b
Tactic: rw [← hb] at han hn
Cleared hypotheses: hn, han, hb
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
hn : 0 < orderOf b
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ orderOf b
hb : orderOf b = n
⊢ orderOf (a * b) = n
have han₁ : orderOf a * orderOf a ∣ orderOf b
Tactic: rw [sq] at han
Cleared hypotheses: han, hb
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ n
⊢ Eq.{u_1 + 1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = n), ball x δ)
have han₁ : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
Tactic: replace han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n := by
    intro b hb
    rw [← hb] at han hn
    rw [sq] at han
    rwa [(Commute.all a b).orderOf_mul_eq_right_of_forall_prime_mul_dvd (orderOf_pos_iff.mp hn)
      fun p _ hp' => dvd_trans (mul_dvd_mul_right hp' <| orderOf a) han]
Cleared hypotheses: han
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : (↑{b : A | orderOf b = n} : Type u_1) → (↑{b : A | orderOf b = n} : Type u_1) :=
  fun (b : (↑{b : A | orderOf b = n} : Type u_1)) ↦
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a * (↑b : A)) ⋯
b : A
hb : Membership.mem (γ := Set A) {b : A | orderOf b = n} b
⊢ ∃ (a : (↑{b : A | orderOf b = n} : Type u_1)),
    f a = Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) b hb
have refine_1 : Membership.mem (γ := Set A) {b : A | orderOf b = n} (a⁻¹ * b)
Tactic: refine ⟨⟨a⁻¹ * b, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : (↑{b : A | orderOf b = n} : Type u_1) → (↑{b : A | orderOf b = n} : Type u_1) :=
  fun (b : (↑{b : A | orderOf b = n} : Type u_1)) ↦
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a * (↑b : A)) ⋯
b : A
hb : Membership.mem (γ := Set A) {b : A | orderOf b = n} b
refine_1 : Membership.mem (γ := Set A) {b : A | orderOf b = n} (a⁻¹ * b)
⊢ ∃ (a : (↑{b : A | orderOf b = n} : Type u_1)),
    f a = Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) b hb
have refine_2 : f (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a⁻¹ * b) sorry) =
  Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) b hb
Tactic: refine ⟨⟨a⁻¹ * b, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : (↑{b : A | orderOf b = n} : Type u_1) → (↑{b : A | orderOf b = n} : Type u_1) :=
  fun (b : (↑{b : A | orderOf b = n} : Type u_1)) ↦
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a * (↑b : A)) ⋯
b : A
hb : Membership.mem (γ := Set A) {b : A | orderOf b = n} b
⊢ Membership.mem (γ := Set A) {b : A | orderOf b = n} (a⁻¹ * b)
have refine_1 : orderOf (a * b⁻¹) = n
Tactic: rw [mem_setOf_eq, ← orderOf_inv, mul_inv_rev, inv_inv, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : (↑{b : A | orderOf b = n} : Type u_1) → (↑{b : A | orderOf b = n} : Type u_1) :=
  fun (b : (↑{b : A | orderOf b = n} : Type u_1)) ↦
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a * (↑b : A)) ⋯
b : A
hb : Membership.mem (γ := Set A) {b : A | orderOf b = n} b
⊢ orderOf (a * b⁻¹) = n
have refine_1 : orderOf b⁻¹ = n
Tactic: apply han
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : (↑{b : A | orderOf b = n} : Type u_1) → (↑{b : A | orderOf b = n} : Type u_1) :=
  fun (b : (↑{b : A | orderOf b = n} : Type u_1)) ↦
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a * (↑b : A)) ⋯
⊢ Eq.{u_1 + 1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = n), ball x δ)
have hf : Surjective f
Tactic: have hf : Surjective f := by
    rintro ⟨b, hb⟩
    refine ⟨⟨a⁻¹ * b, ?_⟩, ?_⟩
    · rw [mem_setOf_eq, ← orderOf_inv, mul_inv_rev, inv_inv, mul_comm]
      apply han
      simpa
    · simp only [f, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ x ∈ approxAddOrderOf UnitAddCircle n δ ↔
    ∃ m < n,
      @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
        ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
have simp : (∃ (b : UnitAddCircle),
    (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1) = b) ∧
      ‖x - b‖ < δ) ↔
  ∃ m < n,
    @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
      ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
Tactic: simp only [mem_approx_add_orderOf_iff, mem_setOf_eq, ball, dist_eq_norm,
    AddCircle.addOrderOf_eq_pos_iff hn, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ (b : UnitAddCircle),
      (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1) = b) ∧
        ‖x - b‖ < δ) ↔
    ∃ m < n,
      @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
        ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
have mp : (∃ (b : UnitAddCircle),
    (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1) = b) ∧
      ‖x - b‖ < δ) →
  ∃ m < n,
    @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
      ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
mp :
  (∃ (b : UnitAddCircle),
      (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1) = b) ∧
        ‖x - b‖ < δ) →
    ∃ m < n,
      @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
        ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
⊢ (∃ (b : UnitAddCircle),
      (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1) = b) ∧
        ‖x - b‖ < δ) ↔
    ∃ m < n,
      @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
        ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
have mpr : (∃ m < n,
    @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
      ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ) →
  ∃ (b : UnitAddCircle),
    (∃ m < n, m.gcd n = 1 ∧ (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1) = b) ∧ ‖x - b‖ < δ
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
⊢ x ∈ addWellApproximable UnitAddCircle δ ↔
    Set.Infinite (α := ℕ)
      {n : ℕ |
        ∃ m < n,
          @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
            ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
have simp : Set.Infinite (α := ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} ↔
  Set.Infinite (α := ℕ)
    {n : ℕ |
      ∃ m < n,
        @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
          ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
Tactic: simp only [mem_add_wellApproximable_iff, ← Nat.cofinite_eq_atTop, cofinite.blimsup_set_eq,
    mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
⊢ Set.Infinite (α := ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} ↔
    Set.Infinite (α := ℕ)
      {n : ℕ |
        ∃ m < n,
          @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
            ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
have refine_1 : ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} n),
  Membership.mem (γ := Set ℕ)
    {n : ℕ |
      ∃ m < n,
        @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
          ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
    n
Tactic: refine iff_of_eq (congr_arg Set.Infinite <| ext fun n => ⟨fun hn => ?_, fun hn => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
refine_1 :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} n),
    Membership.mem (γ := Set ℕ)
      {n : ℕ |
        ∃ m < n,
          @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
            ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
      n
⊢ Set.Infinite (α := ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} ↔
    Set.Infinite (α := ℕ)
      {n : ℕ |
        ∃ m < n,
          @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
            ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
have refine_2 : ∀ (n : ℕ)
  (hn :
    Membership.mem (γ := Set ℕ)
      {n : ℕ |
        ∃ m < n,
          @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
            ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
      n),
  Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} n
Tactic: refine iff_of_eq (congr_arg Set.Infinite <| ext fun n => ⟨fun hn => ?_, fun hn => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    {n : ℕ |
      ∃ m < n,
        @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
          ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
    n
⊢ 0 < n
have obtain : ∀ (m : ℕ) (hm₁ : m < n),
  @gcd _ Nat.instCommMonoidWithZero _ m n = 1 →
    ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n → 0 < n
Tactic: obtain ⟨m, hm₁, _, _⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    {n : ℕ |
      ∃ m < n,
        @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
          ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n}
    n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} n
have h : 0 < n
Tactic: have h : 0 < n := by obtain ⟨m, hm₁, _, _⟩ := hn; exact pos_of_gt hm₁
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊) ∂μ, addWellApproximable 𝕊 δ x
have hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
Tactic: have hu₀ : ∀ p : Nat.Primes, addOrderOf (u p) = (p : ℕ) := by
    rintro ⟨p, hp⟩; exact addOrderOf_div_of_gcd_eq_one hp.pos (gcd_one_left p)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
⊢ Tendsto (addOrderOf ∘ u) atTop atTop
have rw : Tendsto (α := Nat.Primes) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) atTop atTop
Tactic: rw [(funext hu₀ : addOrderOf ∘ u = (↑))]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
⊢ Tendsto (α := Nat.Primes) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) atTop atTop
have h_mono : Monotone (α := { p : ℕ // Nat.Prime p }) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p))
Tactic: have h_mono : Monotone ((↑) : Nat.Primes → ℕ) := fun p q hpq => hpq