awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.WellApproximable
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)
h : ball (b ^ m) ((↑m : ℝ) * δ) = ball (b ^ m) (m • δ)
⊢ (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) ((↑m : ℝ) * δ)

Tactic:
convert! pow_mem_ball hm hab using 1

Premises used: pow_mem_ball
-- Module: Mathlib.NumberTheory.WellApproximable
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)
⊢ ball (b ^ m) ((↑m : ℝ) * δ) = ball (b ^ m) (m • δ)

Tactic:
simp only [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
simp_rw :
  Subset.{u_1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ)
⊢ a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ

Tactic:
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_setOf_eq]

Premises used: Metric.thickening_eq_biUnion_ball, Set.image_smul, smul_ball'', Set.mem_setOf_eq, approxOrderOf, Set.image_iUnion₂, smul_eq_mul
-- Module: Mathlib.NumberTheory.WellApproximable
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 δ)

Tactic:
iUnion₂_subset_iff.mpr fun b hb c hc => ?_

Premises used: Iff.mpr, Set.iUnion₂_subset_iff
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
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
⊢ Subset.{u_1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ)

Tactic:
refine iUnion₂_subset_iff.mpr fun b hb c hc => ?_

Premises used: Iff.mpr, Set.iUnion₂_subset_iff
-- Module: Mathlib.NumberTheory.WellApproximable
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) δ
simp : ∃ (i : A), orderOf i = orderOf a * n ∧ c ∈ ball i δ
⊢ Membership.mem (γ := Set A) (⋃ (x : A), ⋃ (_ : orderOf x = orderOf a * n), ball x δ) c

Tactic:
simp only [mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.NumberTheory.WellApproximable
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 δ

Tactic:
⟨a * b, ?_, hc⟩

Premises used: HMul.hMul, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.WellApproximable
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) δ
refine : orderOf (a * b) = orderOf a * n
⊢ ∃ (i : A), orderOf i = orderOf a * n ∧ c ∈ ball i δ

Tactic:
refine ⟨a * b, ?_, hc⟩
-- Module: Mathlib.NumberTheory.WellApproximable
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) δ
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
⊢ orderOf (a * b) = orderOf a * n

Tactic:
rw [← hb] at han ⊢
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
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:
(Commute.all a b).orderOf_mul_eq_mul_orderOf_of_coprime han

Premises used: Commute.orderOf_mul_eq_mul_orderOf_of_coprime, Commute.all
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
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:
exact (Commute.all a b).orderOf_mul_eq_mul_orderOf_of_coprime han

Premises used: Commute.orderOf_mul_eq_mul_orderOf_of_coprime, Commute.all
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ n
simp_rw :
  Eq.{u_1 + 1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = n), ball x δ)
⊢ a • approxOrderOf A n δ = approxOrderOf A n δ

Tactic:
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_setOf_eq]

Premises used: Metric.thickening_eq_biUnion_ball, Set.image_smul, smul_ball'', Set.mem_setOf_eq, approxOrderOf, Set.image_iUnion₂, smul_eq_mul
-- Module: Mathlib.NumberTheory.WellApproximable
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
⊢ 0 < orderOf b

Tactic:
rw [← hb] at han hn
-- Module: Mathlib.NumberTheory.WellApproximable
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
⊢ HPow.hPow (β := ℕ) (orderOf a) 2 ∣ orderOf b

Tactic:
rw [← hb] at han hn
-- Module: Mathlib.NumberTheory.WellApproximable
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
han₁ : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ orderOf b
⊢ orderOf b = n

Tactic:
rw [← hb] at han hn
-- Module: Mathlib.NumberTheory.WellApproximable
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 * orderOf a ∣ orderOf b

Tactic:
rw [sq] at han

Premises used: sq
-- Module: Mathlib.NumberTheory.WellApproximable
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
han₁ : orderOf a * orderOf a ∣ orderOf b
⊢ orderOf b = n

Tactic:
rw [sq] at han

Premises used: sq
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
hn : 0 < orderOf b
han : orderOf a * orderOf a ∣ orderOf b
hb rwa rwa₁ rwa₂ rwa₃ : orderOf b = n
⊢ orderOf (a * b) = n

Tactic:
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]

Premises used: mul_dvd_mul_right, dvd_trans, orderOf, orderOf_pos_iff, Iff.mp, Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd, Commute.all
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : HPow.hPow (β := ℕ) (orderOf a) 2 ∣ n
⊢ ∀ {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]
-- Module: Mathlib.NumberTheory.WellApproximable
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

Tactic:
⟨⟨a⁻¹ * b, ?_⟩, ?_⟩

Premises used: HMul.hMul, Subtype.mk, Inv.inv, Exists.intro
-- Module: Mathlib.NumberTheory.WellApproximable
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)
refine_2 :
  f (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a⁻¹ * b) ⋯) =
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) b hb
⊢ ∃ (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

Tactic:
refine ⟨⟨a⁻¹ * b, ?_⟩, ?_⟩
-- Module: Mathlib.NumberTheory.WellApproximable
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 : orderOf (a * b⁻¹) = n
⊢ Membership.mem (γ := Set A) {b : A | orderOf b = n} (a⁻¹ * b)

Tactic:
rw [mem_setOf_eq, ← orderOf_inv, mul_inv_rev, inv_inv, mul_comm]

Premises used: Set.mem_setOf_eq, inv_inv, mul_comm, orderOf_inv, mul_inv_rev
-- Module: Mathlib.NumberTheory.WellApproximable
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 : orderOf b⁻¹ = n
⊢ orderOf (a * b⁻¹) = n

Tactic:
apply han
-- Module: Mathlib.NumberTheory.WellApproximable
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 b⁻¹ = n

Tactic:
simpa
-- Module: Mathlib.NumberTheory.WellApproximable
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
⊢ f (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) (a⁻¹ * b) ⋯) =
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) {b : A | orderOf b = n} x) b hb

Tactic:
simp only [f, mul_inv_cancel_left]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.NumberTheory.WellApproximable
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)) ⋯
⊢ 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]
-- Module: Mathlib.NumberTheory.WellApproximable
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)) ⋯
hf : Surjective f
⊢ Eq.{u_1 + 1} (α := Set A) (⋃ (i : A), ⋃ (_ : orderOf i = n), ball (a * i) δ)
    (⋃ (x : A), ⋃ (_ : orderOf x = n), ball x δ)

Tactic:
simpa only [mem_setOf_eq, Subtype.coe_mk, iUnion_coe_set] using
    hf.iUnion_comp fun b => ball (b : A) δ

Premises used: Subtype.coe_mk, Set.iUnion_coe_set, Metric.ball, Set.mem_setOf_eq, Function.Surjective.iUnion_comp, Subtype.val
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
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)‖ < δ
⊢ x ∈ approxAddOrderOf UnitAddCircle n δ ↔
    ∃ 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]

Premises used: dist_eq_norm, Metric.ball, mem_approx_add_orderOf_iff, Set.mem_setOf_eq, AddCircle.addOrderOf_eq_pos_iff, mul_one
-- Module: Mathlib.NumberTheory.WellApproximable
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)‖ < δ
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‖ < δ
⊢ (∃ (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
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
⊢ ∃ m < n,
    @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
      ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ

Tactic:
⟨m, hm₁, hm₂, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ
⊢ ∃ m < n,
    @gcd _ Nat.instCommMonoidWithZero _ m n = 1 ∧
      ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ

Tactic:
exact ⟨m, hm₁, hm₂, hx⟩
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : @gcd _ Nat.instCommMonoidWithZero _ m n = 1
hx : ‖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:
⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩

Premises used: QuotientAddGroup.mk, HDiv.hDiv, Nat.cast, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : @gcd _ Nat.instCommMonoidWithZero _ m n = 1
hx : ‖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:
exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
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}
⊢ x ∈ addWellApproximable UnitAddCircle δ ↔
    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]

Premises used: Set.mem_setOf_eq, mem_add_wellApproximable_iff, Filter.cofinite.blimsup_set_eq, Nat.cofinite_eq_atTop
-- Module: Mathlib.NumberTheory.WellApproximable
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}

Tactic:
iff_of_eq (congr_arg Set.Infinite <| ext fun n => ⟨fun hn => ?_, fun hn => ?_⟩)

Premises used: Set.ext, congr_arg, Iff.intro, Set.Infinite, iff_of_eq
-- Module: Mathlib.NumberTheory.WellApproximable
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
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
⊢ 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:
refine iff_of_eq (congr_arg Set.Infinite <| ext fun n => ⟨fun hn => ?_, fun hn => ?_⟩)

Premises used: Set.ext, congr_arg, Iff.intro, Set.Infinite, iff_of_eq
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
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:
(mem_approxAddOrderOf_iff hn.1).mp hn.2

Premises used: Set.Mem, setOf, UnitAddCircle.mem_approxAddOrderOf_iff, And.right, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
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:
exact (mem_approxAddOrderOf_iff hn.1).mp hn.2

Premises used: UnitAddCircle.mem_approxAddOrderOf_iff, And.right, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.WellApproximable
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
obtain :
  ∀ (m : ℕ) (hm₁ : m < n),
    @gcd _ Nat.instCommMonoidWithZero _ m n = 1 →
      ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n → 0 < n
⊢ 0 < n

Tactic:
obtain ⟨m, hm₁, _, _⟩ := hn
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left : @gcd _ Nat.instCommMonoidWithZero _ m n = 1
right : ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n
⊢ 0 < n

Tactic:
pos_of_gt hm₁

Premises used: pos_of_gt
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
δ : ℕ → ℝ
x : UnitAddCircle
n m : ℕ
hm₁ : m < n
left : @gcd _ Nat.instCommMonoidWithZero _ m n = 1
right : ‖x - (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) : ℝ ⧸ AddSubgroup.zmultiples 1)‖ < δ n
⊢ 0 < n

Tactic:
exact pos_of_gt hm₁

Premises used: pos_of_gt
-- Module: Mathlib.NumberTheory.WellApproximable
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

Tactic:
have h : 0 < n := by obtain ⟨m, hm₁, _, _⟩ := hn; exact pos_of_gt hm₁
-- Module: Mathlib.NumberTheory.WellApproximable
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
h : 0 < n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} n

Tactic:
⟨h, (mem_approxAddOrderOf_iff h).mpr hn⟩

Premises used: Iff.mpr, Set.Mem, setOf, UnitAddCircle.mem_approxAddOrderOf_iff, And.intro
-- Module: Mathlib.NumberTheory.WellApproximable
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
h : 0 < n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)} n

Tactic:
exact ⟨h, (mem_approxAddOrderOf_iff h).mpr hn⟩
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
set :
  let μ : Measure 𝕊 := volume;
  (∀ᵐ (x : 𝕊) ∂μ, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊) ∂μ, addWellApproximable 𝕊 δ x
⊢ (∀ᵐ (x : 𝕊), ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊), addWellApproximable 𝕊 δ x

Tactic:
set μ : Measure 𝕊 := volume

Premises used: MeasureTheory.MeasureSpace.volume