awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₈ : |p / 2| = |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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₉ : |p| / |2| = |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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₁₀ : |p| / 2 = |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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
hp : p ≠ 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x| ↔ |x| ≤ |p| / 2
have refine : ∀ (hx : |x| ≤ |p| / 2),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
Tactic: refine ⟨fun hx => hx ▸ norm_le_half_period p hp, fun hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
have inl : ∀ (hp : 0 < p), norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
Tactic: rcases hp.symm.lt_or_gt with (hp | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
have inr : ∀ (hp : p < 0), norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
Tactic: rcases hp.symm.lt_or_gt with (hp | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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|
have hx₁ : |x| ≤ p / 2
Tactic: rw [abs_eq_self.mpr hp.le] at hx
Cleared hypotheses: hx, this, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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|
have inr : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) = |x|
Tactic: rw [← norm_neg_period]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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|
have hx₁ : |x| ≤ -p / 2
Tactic: rw [abs_eq_neg_self.mpr hp.le] at hx
Cleared hypotheses: hx, this, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
have suffices : ∀ (p : ℝ),
  0 < p →
    |x| ≤ p / 2 → 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
have inl : ∀ (hx : |p / 2| ≤ p / 2),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p / 2|
Tactic: rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
have inr : ∀ (hx' : x ≠ p / 2),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
Tactic: rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) = |x|
have inr : round (p⁻¹ * x) = 0
Tactic: suffices round (p⁻¹ * x) = 0 by simp [norm_eq, this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ round (p⁻¹ * x) = 0
have inr : p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
Tactic: rw [round_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p_1 x : ℝ
hp_1 : p_1 ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
have hx₁ : -(p / 2) ≤ x
Tactic: obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
have hx₂ : x ≤ p / 2
Tactic: obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
have hx₃ : x < p / 2
Tactic: replace hx₂ := Ne.lt_of_le hx' hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
have inr : -(1 / 2) ≤ p⁻¹ * x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
have inr₁ : p⁻¹ * x < 1 / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ -(1 / 2) ≤ p⁻¹ * x
have inr : p * -(1 / 2) ≤ x
Tactic: rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ -(1 / 2) ≤ p⁻¹ * x
have inr₁ : -(p * (1 / 2)) ≤ x
Tactic: rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ -(1 / 2) ≤ p⁻¹ * x
have inr₂ : -(p * 1 / 2) ≤ x
Tactic: rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p⁻¹ * x < 1 / 2
have inr : x < p * (1 / 2)
Tactic: rwa [inv_mul_lt_iff₀ hp, ← mul_div_assoc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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)
⊢ p⁻¹ * x < 1 / 2
have inr₁ : x < p * 1 / 2
Tactic: rwa [inv_mul_lt_iff₀ hp, ← mul_div_assoc, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x ε : ℝ
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) =
    closedBall x ε
have h : ∀ (y : ℝ),
  y ∈
      preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ↔
    y ∈ closedBall x ε
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples p) ε) =
    ⋃ (z : ℤ), closedBall (x + z • p) ε
have inl : preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
    (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) =
  ⋃ (z : ℤ), closedBall (x + HSMul.hSMul (β := ℝ) z 0) ε
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
inl :
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) =
    ⋃ (z : ℤ), closedBall (x + HSMul.hSMul (β := ℝ) z 0) ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples p) ε) =
    ⋃ (z : ℤ), closedBall (x + z • p) ε
have inr : ∀ (hp : p ≠ 0),
  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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
hp : p ≠ 0
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples p) ε) =
    ⋃ (z : ℤ), closedBall (x + z • p) ε
have inr : ∀ (y : ℝ),
  y ∈
      preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ↔
    Membership.mem (γ := Set ℝ) (⋃ (z : ℤ), closedBall (x + z • p) ε) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈
      preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ↔
    Membership.mem (γ := Set ℝ) (⋃ (z : ℤ), closedBall (x + z • p) ε) y
have inr : |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε ↔ ∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε
Tactic: simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
    ← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε ↔ ∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε
have inr : (∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε) → |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε
Tactic: refine ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |y - x - (↑n : ℝ) * p| ≤ ε
⊢ |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε
have inr : ∀ (hn : |p⁻¹ * (y - x) - (↑n : ℝ)| ≤ |p⁻¹| * ε), |p⁻¹ * (y - x) - (↑(round (p⁻¹ * (y - x))) : ℝ)| ≤ |p⁻¹| * ε
Tactic: rw [← mul_le_mul_iff_right₀ (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p,
    inv_mul_cancel_left₀ hp] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
have inl : ∀ (hε : |p| / 2 ≤ ε),
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
Tactic: rcases le_or_gt (|p| / 2) ε with hε | hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
inl :
  ∀ (hε : |p| / 2 ≤ ε),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
        s =
      if ε < |p| / 2 then closedBall x ε ∩ s else s
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
have inr : ∀ (hε : ε < |p| / 2),
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
Tactic: rcases le_or_gt (|p| / 2) ε with hε | hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
have inl : ∀ (hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)) (hε : HDiv.hDiv (α := ℝ) |0| 2 ≤ ε),
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ∩
      s =
    if ε < HDiv.hDiv (α := ℝ) |0| 2 then closedBall x ε ∩ s else s
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
Cleared hypotheses: p, hs, hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
inl :
  ∀ (hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)) (hε : HDiv.hDiv (α := ℝ) |0| 2 ≤ ε),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ∩
        s =
      if ε < HDiv.hDiv (α := ℝ) |0| 2 then closedBall x ε ∩ s else s
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
have inl₁ : ∀ (hp : p ≠ 0),
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)
hε : HDiv.hDiv (α := ℝ) |0| 2 ≤ ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ∩
      s =
    if ε < HDiv.hDiv (α := ℝ) |0| 2 then closedBall x ε ∩ s else s
have hε₁ : 0 ≤ ε
Tactic: simp only [abs_zero, zero_div] at hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)
hε : 0 ≤ ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ∩
      s =
    if ε < HDiv.hDiv (α := ℝ) |0| 2 then closedBall x ε ∩ s else s
have inl : s ⊆ closedBall x ε
Tactic: simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div,
        if_false, inter_eq_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s
have inr : ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
Tactic: suffices ∀ z : ℤ, closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅ by
      simp [-zsmul_eq_mul, coe_real_preimage_closedBall_eq_iUnion,
        iUnion_inter, iUnion_ite, this, hε]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
have inr : ∀ (hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)),
  Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
Tactic: simp only [Real.closedBall_eq_Icc] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
have inr : Icc (x + HSMul.hSMul (α := ℤ) 0 p - ε) (x + HSMul.hSMul (α := ℤ) 0 p + ε) ∩ s =
  if Eq (α := ℤ) 0 0 then Icc (x - ε) (x + ε) ∩ s else ∅
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
inr :
  Icc (x + HSMul.hSMul (α := ℤ) 0 p - ε) (x + HSMul.hSMul (α := ℤ) 0 p + ε) ∩ s =
    if Eq (α := ℤ) 0 0 then Icc (x - ε) (x + ε) ∩ s else ∅
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
have inr₁ : ∀ (hz : z ≠ 0), Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
have inr : ∀ (x_1 : ℝ), x_1 ∉ Icc (x + (↑z : ℝ) * p - ε) (x + (↑z : ℝ) * p + ε) ∩ s
Tactic: simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
⊢ False
have hy₃ : x - |p| / 2 ≤ y
Tactic: obtain ⟨hy₃, hy₄⟩ := hs hy₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
⊢ False
have hy₄ : y ≤ x + |p| / 2
Tactic: obtain ⟨hy₃, hy₄⟩ := hs hy₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
⊢ False
have inr : ∀ (hp : 0 < p), False
Tactic: rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
inr : ∀ (hp : 0 < p), False
⊢ False
have inr₁ : ∀ (hε : ε < HDiv.hDiv (α := ℝ) |0| 2) (hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2))
  (hy₁ : x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 - ε ≤ y) (hy₂ : y ≤ x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 + ε)
  (hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y) (hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2), False
Tactic: rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)
Cleared hypotheses: p, hε, hs, hy₁, hy₂, hy₃, hy₄
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
inr : ∀ (hp : 0 < p), False
inr₁ :
  ∀ (hε : ε < HDiv.hDiv (α := ℝ) |0| 2) (hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2))
    (hy₁ : x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 - ε ≤ y) (hy₂ : y ≤ x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 + ε)
    (hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y) (hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2), False
⊢ False
have inr₂ : ∀ (hp : p < 0), False
Tactic: rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)