awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
suffices :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|

Tactic:
suffices ∀ x : ℝ, ‖(x : AddCircle (1 : ℝ))‖ = |x - round x| by
    rcases eq_or_ne p 0 with (rfl | hp)
    · simp
    have hx := norm_coe_mul p x p⁻¹
    rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
    rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
simp :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) ≤
      |x - (↑(round x) : ℝ)| ∧
    ∀ (m : ℝ),
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
          (↑x : ℝ ⧸ zmultiples 1) →
        |x - (↑(round x) : ℝ)| ≤ |m|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
    |x - (↑(round x) : ℝ)|

Tactic:
simp only [le_antisymm_iff, le_norm_iff, Real.norm_eq_abs]

Premises used: QuotientAddGroup.le_norm_iff, le_antisymm_iff, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) ≤
      |x - (↑(round x) : ℝ)| ∧
    ∀ (m : ℝ),
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
          (↑x : ℝ ⧸ zmultiples 1) →
        |x - (↑(round x) : ℝ)| ≤ |m|

Tactic:
⟨le_of_forall_le fun r hr ↦ ?_, ?_⟩

Premises used: le_of_forall_le, And.intro
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
refine_1 :
  ∀ (r : ℝ) (hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)),
    r ≤ |x - (↑(round x) : ℝ)|
refine_2 :
  ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      |x - (↑(round x) : ℝ)| ≤ |m|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) ≤
      |x - (↑(round x) : ℝ)| ∧
    ∀ (m : ℝ),
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
          (↑x : ℝ ⧸ zmultiples 1) →
        |x - (↑(round x) : ℝ)| ≤ |m|

Tactic:
refine ⟨le_of_forall_le fun r hr ↦ ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x r : ℝ
hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)
refine_1 : r ≤ fract x ∧ r ≤ 1 - fract x
⊢ r ≤ |x - (↑(round x) : ℝ)|

Tactic:
rw [abs_sub_round_eq_min, le_inf_iff]

Premises used: abs_sub_round_eq_min, le_inf_iff
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x r : ℝ
hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)
⊢ ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      r ≤ ‖m‖

Tactic:
rw [le_norm_iff] at hr

Premises used: QuotientAddGroup.le_norm_iff
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x r : ℝ
hr :
  ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      r ≤ ‖m‖
refine_1 : r ≤ fract x
refine_1₁ : r ≤ 1 - fract x
⊢ r ≤ fract x ∧ r ≤ 1 - fract x

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x r : ℝ
hr :
  ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      r ≤ ‖m‖
⊢ r ≤ fract x

Tactic:
simpa [abs_of_nonneg] using hr (fract x)

Premises used: Int.fract, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x r : ℝ
hr :
  ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      r ≤ ‖m‖
⊢ Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(fract x - 1) : ℝ ⧸ zmultiples 1)
    (↑x : ℝ ⧸ zmultiples 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x r : ℝ
hr :
  ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      r ≤ ‖m‖
⊢ r ≤ 1 - fract x

Tactic:
simpa [abs_sub_comm (fract x)] using hr (fract x - 1) (by simp)

Premises used: Int.fract, HSub.hSub, abs_sub_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
⊢ ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      |x - (↑(round x) : ℝ)| ≤ |m|

Tactic:
simpa [zmultiples, QuotientAddGroup.eq, zsmul_eq_mul, mul_one, mem_mk, mem_range, and_imp,
      forall_exists_index, eq_neg_add_iff_add_eq, ← eq_sub_iff_add_eq, forall_comm (α := ℕ)]
      using round_le _

Premises used: zsmul_eq_mul, Set.mem_range, QuotientAddGroup.eq, and_imp, eq_sub_iff_add_eq, forall_comm, forall_exists_index, round_le, AddSubgroup.mem_mk, eq_neg_add_iff_add_eq, AddSubgroup.zmultiples, mul_one
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : 0 < p
x : ℝ
a : p
a₁ : |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
| p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : 0 < p
x : ℝ
a : |p|
| p

Tactic:
rw [← abs_eq_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : 0 < p
x : ℝ
a : |p|
a₁ : |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
| p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|

Tactic:
congr
    rw [← abs_eq_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : 0 < p
x : ℝ
conv_rhs :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|

Tactic:
conv_rhs =>
    congr
    rw [← abs_eq_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : 0 < p
x : ℝ
rw :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p * (p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ))|
rw₁ :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p * (p⁻¹ * x) - p * (↑(round (p⁻¹ * x)) : ℝ)|
rw₂ :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - p * (↑(round (p⁻¹ * x)) : ℝ)|
rw₃ : |x - (↑(round (p⁻¹ * x)) : ℝ) * p| = |x - p * (↑(round (p⁻¹ * x)) : ℝ)|
rw₄ rw₅ : |x - (↑(round (p⁻¹ * x)) : ℝ) * p| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|

Tactic:
rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]

Premises used: mul_inv_cancel_left₀, mul_sub, abs_mul, Ne.symm, mul_comm, AddCircle.norm_eq, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
x : AddCircle p
hp : p ≠ 0
mk : ∀ (x : ℝ), norm (E := AddCircle p) (Quot.mk (⇑(leftRel (zmultiples p)) : ℝ → ℝ → Prop) x) ≤ |p| / 2
⊢ ‖x‖ ≤ |p| / 2

Tactic:
obtain ⟨x⟩ := x
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
x_1 : AddCircle p
hp : p ≠ 0
x : ℝ
mk : |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| ≤ 1 / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) ≤ |p| / 2

Tactic:
rw [norm_eq, ← mul_le_mul_iff_right₀ (abs_pos.mpr (inv_ne_zero hp)), ← abs_mul, mul_sub,
    mul_left_comm, ← mul_div_assoc, ← abs_mul, inv_mul_cancel₀ hp, mul_one, abs_one]

Premises used: Iff.mpr, mul_sub, mul_div_assoc, abs_mul, mul_left_comm, abs_pos, inv_ne_zero, AddCircle.norm_eq, mul_one, abs_one, inv_mul_cancel₀, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
x_1 : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| ≤ 1 / 2

Tactic:
abs_sub_round (p⁻¹ * x)

Premises used: abs_sub_round, HMul.hMul, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
x_1 : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| ≤ 1 / 2

Tactic:
exact abs_sub_round (p⁻¹ * x)

Premises used: abs_sub_round, HMul.hMul, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
inl :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑(0 / 2) : ℝ ⧸ zmultiples 0) =
    HDiv.hDiv (α := ℝ) |0| 2
inr :
  ∀ (hp : p ≠ 0),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑(0 / 2) : ℝ ⧸ zmultiples 0) =
    HDiv.hDiv (α := ℝ) |0| 2

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : p ≠ 0
linarith : p / 2 - p < -(p / 2) → 2 / 2 = 1
linarith₁ : p / 2 - p < -(p / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : p / 2 - p < -(p / 2) → 2 / 2 = 1
linarith₃ : p / 2 - p < -(p / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : p / 2 - p < -(p / 2) → GT.gt (α := ℝ) 2 0
linarith₅ : p / 2 - p < -(p / 2) → 1 * p - 2 * p - -(1 * p) = 0
linarith₆ : -(p / 2) < p / 2 - p → 2 / 2 = 1
linarith₇ : -(p / 2) < p / 2 - p → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : -(p / 2) < p / 2 - p → 2 / 2 = 1
linarith₉ : -(p / 2) < p / 2 - p → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : -(p / 2) < p / 2 - p → GT.gt (α := ℝ) 2 0
linarith₁₁ : -(p / 2) < p / 2 - p → -(1 * p) - (1 * p - 2 * p) = 0
⊢ p / 2 - p = -(p / 2)

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : p ≠ 0
inr : |p / 2 - (↑(round (p⁻¹ * (p / 2))) : ℝ) * p| = |p| / 2
inr₁ : |p / 2 - (↑(round (p⁻¹ * p / 2)) : ℝ) * p| = |p| / 2
inr₂ : |p / 2 - (↑(round (1 / 2)) : ℝ) * p| = |p| / 2
inr₃ : |p / 2 - (↑(round (α := ℝ) 2⁻¹) : ℝ) * p| = |p| / 2
inr₄ : |p / 2 - (↑1 : ℝ) * p| = |p| / 2
inr₅ : |p / 2 - 1 * p| = |p| / 2
inr₆ : |p / 2 - p| = |p| / 2
inr₇ : |(-(p / 2))| = |p| / 2
inr₈ : |p / 2| = |p| / 2
inr₉ : |p| / |2| = |p| / 2
inr₁₀ inr₁₁ : |p| / 2 = |p| / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2

Tactic:
rw [norm_eq, ← mul_div_assoc, inv_mul_cancel₀ hp, one_div, round_two_inv, Int.cast_one,
    one_mul, (by linarith : p / 2 - p = -(p / 2)), abs_neg, abs_div, abs_two]

Premises used: abs_neg, round_two_inv, mul_div_assoc, abs_div, one_div, AddCircle.norm_eq, inv_mul_cancel₀, one_mul, Int.cast_one, abs_two
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp : p ≠ 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x| ↔ |x| ≤ |p| / 2

Tactic:
⟨fun hx => hx ▸ norm_le_half_period p hp, fun hx => ?_⟩

Premises used: Eq.rec, Iff.intro, AddCircle.norm_le_half_period
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp : p ≠ 0
refine :
  ∀ (hx : |x| ≤ |p| / 2),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x| ↔ |x| ≤ |p| / 2

Tactic:
refine ⟨fun hx => hx ▸ norm_le_half_period p hp, fun hx => ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
inl :
  ∀ (hp : 0 < p), norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
inr :
  ∀ (hp : p < 0), norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
rcases hp.symm.lt_or_gt with (hp | hp)

Premises used: Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : 0 < p
⊢ |x| ≤ p / 2

Tactic:
rw [abs_eq_self.mpr hp.le] at hx

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : 0 < p
hx₁ : |x| ≤ p / 2
⊢ ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
rw [abs_eq_self.mpr hp.le] at hx

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : 0 < p
hx₁ : |x| ≤ p / 2
this₁ :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
⊢ 0 < p

Tactic:
rw [abs_eq_self.mpr hp.le] at hx

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ p / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : 0 < p
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
this p hp hx
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ p / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : 0 < p
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
exact this p hp hx
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : p < 0
inr : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) = |x|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
rw [← norm_neg_period]

Premises used: AddCircle.norm_neg_period
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : p < 0
⊢ |x| ≤ -p / 2

Tactic:
rw [abs_eq_neg_self.mpr hp.le] at hx

Premises used: Iff.mpr, LT.lt.le, abs_eq_neg_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : p < 0
hx₁ : |x| ≤ -p / 2
⊢ ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
rw [abs_eq_neg_self.mpr hp.le] at hx

Premises used: Iff.mpr, LT.lt.le, abs_eq_neg_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ |p| / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : p < 0
hx₁ : |x| ≤ -p / 2
this₁ :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
⊢ p < 0

Tactic:
rw [abs_eq_neg_self.mpr hp.le] at hx

Premises used: Iff.mpr, LT.lt.le, abs_eq_neg_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ -p / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : p < 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) = |x|

Tactic:
this (-p) (neg_pos.mpr hp) hx

Premises used: Iff.mpr, neg_pos, Neg.neg
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp_1 : p ≠ 0
hx : |x| ≤ -p / 2
this :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
hp : p < 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) = |x|

Tactic:
exact this (-p) (neg_pos.mpr hp) hx

Premises used: Iff.mpr, neg_pos, Neg.neg
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
suffices :
  ∀ (p : ℝ),
    0 < p →
      |x| ≤ p / 2 → norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
suffices ∀ p : ℝ, 0 < p → |x| ≤ p / 2 → ‖(x : AddCircle p)‖ = |x| by
    rcases hp.symm.lt_or_gt with (hp | hp)
    · rw [abs_eq_self.mpr hp.le] at hx
      exact this p hp hx
    · rw [← norm_neg_period]
      rw [abs_eq_neg_self.mpr hp.le] at hx
      exact this (-p) (neg_pos.mpr hp) hx
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
inl :
  ∀ (hx : |p / 2| ≤ p / 2),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p / 2|
inr :
  ∀ (hx' : x ≠ p / 2),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')

Premises used: HDiv.hDiv, eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |p / 2| ≤ p / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p / 2|

Tactic:
simp [abs_div]

Premises used: abs_div
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
this : round (p⁻¹ * x) = 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
simp [norm_eq, this]

Premises used: AddCircle.norm_eq
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
inr : round (p⁻¹ * x) = 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|

Tactic:
suffices round (p⁻¹ * x) = 0 by simp [norm_eq, this]
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
inr : p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
⊢ round (p⁻¹ * x) = 0

Tactic:
rw [round_eq_zero_iff]

Premises used: round_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ -(p / 2) ≤ x

Tactic:
obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx

Premises used: abs_le, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
⊢ x ≤ p / 2

Tactic:
obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx

Premises used: abs_le, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x ≤ p / 2
⊢ x < p / 2

Tactic:
replace hx₂ := Ne.lt_of_le hx' hx₂
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
inr : -(1 / 2) ≤ p⁻¹ * x
inr₁ : p⁻¹ * x < 1 / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
inr : p * -(1 / 2) ≤ x
inr₁ : -(p * (1 / 2)) ≤ x
inr₂ : -(p * 1 / 2) ≤ x
inr₃ inr₄ inr₅ inr₆ : -(p / 2) ≤ x
⊢ -(1 / 2) ≤ p⁻¹ * x

Tactic:
rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]

Premises used: mul_div_assoc, le_inv_mul_iff₀, mul_one, mul_neg
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
inr : x < p * (1 / 2)
inr₁ : x < p * 1 / 2
inr₂ inr₃ inr₄ inr₅ : x < p / 2
⊢ p⁻¹ * x < 1 / 2

Tactic:
rwa [inv_mul_lt_iff₀ hp, ← mul_div_assoc, mul_one]

Premises used: mul_div_assoc, inv_mul_lt_iff₀, mul_one
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : p ≠ 0
x_1 : AddCircle p
ε : ℝ
hε : |p| / 2 ≤ ε
x : AddCircle p
⊢ x ∈ closedBall x_1 ε

Tactic:
simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε

Premises used: dist_eq_norm, AddCircle.norm_le_half_period, Metric.mem_closedBall, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
h :
  ∀ (y : ℝ),
    y ∈
        preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ↔
      y ∈ closedBall x ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) =
    closedBall x ε

Tactic:
ext y
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε y : ℝ
⊢ y ∈
      preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ↔
    y ∈ closedBall x ε

Tactic:
simp [dist_eq_norm, ← QuotientAddGroup.mk_sub]

Premises used: dist_eq_norm, QuotientAddGroup.mk_sub
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
inl :
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) =
    ⋃ (z : ℤ), closedBall (x + HSMul.hSMul (β := ℝ) z 0) ε
inr :
  ∀ (hp : p ≠ 0),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) =
      ⋃ (z : ℤ), closedBall (x + z • p) ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples p) ε) =
    ⋃ (z : ℤ), closedBall (x + z • p) ε

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) =
    ⋃ (z : ℤ), closedBall (x + HSMul.hSMul (β := ℝ) z 0) ε

Tactic:
simp [iUnion_const]

Premises used: Set.iUnion_const