p x : ℝ
hp : p ≠ 0
hx : abs x ≤ abs p / 2
⊢ ‖↑x‖ = abs x
p x : ℝ
hp : p ≠ 0
⊢ ‖↑x‖ = abs x ↔ abs x ≤ abs p / 2
refine' ⟨fun hx => hx ▸ norm_le_half_period p hp, fun hx => _⟩
p x : ℝ
hp : p ≠ 0
⊢ ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
p x : ℝ
hp : p ≠ 0
hx : abs x ≤ abs p / 2
⊢ ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
clear hx
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
⊢ ‖↑x‖ = abs x
p x : ℝ
hp : p ≠ 0
⊢ ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
intro p hp hx
case inl
p✝ : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs (p / 2) ≤ p / 2
⊢ ‖↑(p / 2)‖ = abs (p / 2)

case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = abs x
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
⊢ ‖↑x‖ = abs x
rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
⊢ round (p⁻¹ * x) = 0
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = abs x
suffices round (p⁻¹ * x) = 0 by simp [norm_eq, this]
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
⊢ round (p⁻¹ * x) = 0
rw [round_eq_zero_iff]
case inr.intro
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x ≤ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx
case inr.intro
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
case inr.intro
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x ≤ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
replace hx₂ := Ne.lt_of_le hx' hx₂
case inr.intro.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x

case inr.intro.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2
case inr.intro
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
constructor
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : 0 < p
⊢ ‖↑x‖ = abs x

case inr
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : p < 0
⊢ ‖↑x‖ = abs x
p x : ℝ
hp : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
⊢ ‖↑x‖ = abs x
rcases hp.symm.lt_or_lt with (hp | hp)
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : 0 < p
⊢ ‖↑x‖ = abs x
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : 0 < p
⊢ ‖↑x‖ = abs x
rw [abs_eq_self.mpr hp.le] at hx
no goals
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : 0 < p
⊢ ‖↑x‖ = abs x
exact this p hp hx
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : p < 0
⊢ ‖↑x‖ = abs x
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : p < 0
⊢ ‖↑x‖ = abs x
rw [← norm_neg_period]
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ -p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : p < 0
⊢ ‖↑x‖ = abs x
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ abs p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : p < 0
⊢ ‖↑x‖ = abs x
rw [abs_eq_neg_self.mpr hp.le] at hx
no goals
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : abs x ≤ -p / 2
this : ∀ (p : ℝ), 0 < p → abs x ≤ p / 2 → ‖↑x‖ = abs x
hp : p < 0
⊢ ‖↑x‖ = abs x
exact this (-p) (neg_pos.mpr hp) hx
no goals
case inl
p✝ : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs (p / 2) ≤ p / 2
⊢ ‖↑(p / 2)‖ = abs (p / 2)
simp [abs_div, abs_two]
no goals
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
this : round (p⁻¹ * x) = 0
⊢ ‖↑x‖ = abs x
simp [norm_eq, this]
no goals
case inr.intro.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x
rwa [← mul_le_mul_left hp, ← mul_assoc, mul_inv_cancel hp.ne.symm, one_mul, mul_neg, ←
  mul_div_assoc, mul_one]
no goals
case inr.intro.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : abs x ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2
rwa [← mul_lt_mul_left hp, ← mul_assoc, mul_inv_cancel hp.ne.symm, one_mul, ← mul_div_assoc,
  mul_one]