awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
inr :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₁ :
  |p| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples 1) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₂ : |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₃ : |p * (p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ))| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr₄ : |p * (p⁻¹ * x) - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
inr :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₁ :
  |p| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples 1) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₂ : |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₃ : |p * (p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ))| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₄ : |p * (p⁻¹ * x) - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr₅ : |x - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
inr :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₁ :
  |p| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples 1) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₂ : |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₃ : |p * (p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ))| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₄ : |p * (p⁻¹ * x) - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₅ : |x - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr₆ : |x - (↑(round (p⁻¹ * x)) : ℝ) * p| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have suffices : ∀ (x : ℝ),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
    |x - (↑(round x) : ℝ)|
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
    |x - (↑(round x) : ℝ)|
have 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|
Tactic: simp only [le_antisymm_iff, le_norm_iff, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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|
have refine_1 : ∀ (r : ℝ) (hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)),
  r ≤ |x - (↑(round x) : ℝ)|
Tactic: refine ⟨le_of_forall_le fun r hr ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x : ℝ
refine_1 :
  ∀ (r : ℝ) (hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)),
    r ≤ |x - (↑(round 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|
have refine_2 : ∀ (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 ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x r : ℝ
hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)
⊢ r ≤ |x - (↑(round x) : ℝ)|
have refine_1 : r ≤ fract x ∧ r ≤ 1 - fract x
Tactic: rw [abs_sub_round_eq_min, le_inf_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
x r : ℝ
hr : r ≤ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1)
⊢ r ≤ fract x ∧ r ≤ 1 - fract x
have hr₁ : ∀ (m : ℝ),
  Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1) (↑x : ℝ ⧸ zmultiples 1) →
    r ≤ ‖m‖
Tactic: rw [le_norm_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x r : ℝ
hr :
  ∀ (m : ℝ),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑m : ℝ ⧸ zmultiples 1)
        (↑x : ℝ ⧸ zmultiples 1) →
      r ≤ ‖m‖
⊢ r ≤ fract x ∧ r ≤ 1 - fract x
have refine_1 : r ≤ fract x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ r ≤ fract x ∧ r ≤ 1 - fract x
have refine_1₁ : r ≤ 1 - fract x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
| p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have a : p
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
a : p
| p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have a₁ : |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
| p
have a : |p|
Tactic: rw [← abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
| p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have a : |p|
Tactic: congr
    rw [← abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
a : |p|
| p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have a₁ : |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
Tactic: congr
    rw [← abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    p * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have conv_rhs : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : 0 < p
x : ℝ
rw :
  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)) : ℝ)|
have rw₁ : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
  |p * (p⁻¹ * x) - p * (↑(round (p⁻¹ * x)) : ℝ)|
Tactic: rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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)) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have rw₂ : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
  |x - p * (↑(round (p⁻¹ * x)) : ℝ)|
Tactic: rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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)) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have rw₃ : |x - (↑(round (p⁻¹ * x)) : ℝ) * p| = |x - p * (↑(round (p⁻¹ * x)) : ℝ)|
Tactic: rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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)) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)|
have rw₄ : |x - (↑(round (p⁻¹ * x)) : ℝ) * p| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
x : AddCircle p
hp : p ≠ 0
⊢ ‖x‖ ≤ |p| / 2
have mk : ∀ (x : ℝ), norm (E := AddCircle p) (Quot.mk (⇑(leftRel (zmultiples p)) : ℝ → ℝ → Prop) x) ≤ |p| / 2
Tactic: obtain ⟨x⟩ := x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
x_1 : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) ≤ |p| / 2
have mk : |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| ≤ 1 / 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inl : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑(0 / 2) : ℝ ⧸ zmultiples 0) =
  HDiv.hDiv (α := ℝ) |0| 2
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 : ℝ
inl :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑(0 / 2) : ℝ ⧸ zmultiples 0) =
    HDiv.hDiv (α := ℝ) |0| 2
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr : ∀ (hp : p ≠ 0),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ p / 2 - p = -(p / 2)
have linarith : p / 2 - p < -(p / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : p ≠ 0
linarith : p / 2 - p < -(p / 2) → 2 / 2 = 1
⊢ p / 2 - p = -(p / 2)
have linarith₁ : p / 2 - p < -(p / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p / 2 - p = -(p / 2)
have linarith₄ : p / 2 - p < -(p / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p / 2 - p = -(p / 2)
have linarith₅ : p / 2 - p < -(p / 2) → 1 * p - 2 * p - -(1 * p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p / 2 - p = -(p / 2)
have linarith₆ : -(p / 2) < p / 2 - p → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p / 2 - p = -(p / 2)
have linarith₇ : -(p / 2) < p / 2 - p → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p / 2 - p = -(p / 2)
have linarith₁₀ : -(p / 2) < p / 2 - p → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p / 2 - p = -(p / 2)
have linarith₁₁ : -(p / 2) < p / 2 - p → -(1 * p) - (1 * p - 2 * p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr : |p / 2 - (↑(round (p⁻¹ * (p / 2))) : ℝ) * 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]
-- 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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₁ : |p / 2 - (↑(round (p⁻¹ * p / 2)) : ℝ) * 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]
-- 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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₂ : |p / 2 - (↑(round (1 / 2)) : ℝ) * 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]
-- 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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₃ : |p / 2 - (↑(round (α := ℝ) 2⁻¹) : ℝ) * 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]
-- 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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₄ : |p / 2 - (↑1 : ℝ) * 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]
-- 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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₅ : |p / 2 - 1 * 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]
-- 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
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑(p / 2) : ℝ ⧸ zmultiples p) = |p| / 2
have inr₆ : |p / 2 - 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]
-- 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
⊢ 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]