⊢ ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
p x : ℝ
⊢ ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
clear! x p
x : ℝ
⊢ ‖↑x‖ = abs (x - ↑(round x))
⊢ ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
intros x
x : ℝ
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
x : ℝ
⊢ ‖↑x‖ = abs (x - ↑(round x))
rw [quotient_norm_eq, abs_sub_round_eq_min]
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
x : ℝ
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
have h₁ : BddBelow (abs '' { m : ℝ | (m : AddCircle (1 : ℝ)) = x }) :=
  ⟨0, by simp [mem_lowerBounds]⟩
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
have h₂ : (abs '' { m : ℝ | (m : AddCircle (1 : ℝ)) = x }).Nonempty := ⟨|x|, ⟨x, rfl, rfl⟩⟩
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) ≤ min (fract x) (1 - fract x)

case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ min (fract x) (1 - fract x) ≤ sInf (norm '' {m | ↑m = ↑x})
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
apply le_antisymm
case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
⊢ ‖↑x‖ = abs (x - ↑(round (0⁻¹ * x)) * 0)

case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
rcases eq_or_ne p 0 with (rfl | hp)
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
intros
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = abs p⁻¹ * ‖↑x‖
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
have hx := norm_coe_mul p x p⁻¹
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
hx : abs p * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = abs p⁻¹ * ‖↑x‖
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
no goals
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
hp : p ≠ 0
hx : abs p * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = abs (x - ↑(round (p⁻¹ * x)) * p)
rw [← hx, inv_mul_cancel hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
no goals
case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = abs (x - ↑(round x))
⊢ ‖↑x‖ = abs (x - ↑(round (0⁻¹ * x)) * 0)
simp
no goals
x : ℝ
⊢ 0 ∈ lowerBounds (abs '' {m | ↑m = ↑x})
simp [mem_lowerBounds]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ ∀ (b : ℝ), b ∈ lowerBounds (abs '' {m | ↑m = ↑x}) → b ≤ fract x ∧ b ≤ 1 - fract x
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) ≤ min (fract x) (1 - fract x)
simp_rw [Real.norm_eq_abs, csInf_le_iff h₁ h₂, le_min_iff]
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ b ≤ fract x ∧ b ≤ 1 - fract x
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ ∀ (b : ℝ), b ∈ lowerBounds (abs '' {m | ↑m = ↑x}) → b ≤ fract x ∧ b ≤ 1 - fract x
intro b h
case a.refine'_1
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x ∈ {m | ↑m = ↑x}

case a.refine'_2
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x - 1 ∈ {m | ↑m = ↑x}
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ b ≤ fract x ∧ b ≤ 1 - fract x
refine'
  ⟨mem_lowerBounds.1 h _ ⟨fract x, _, abs_fract⟩,
    mem_lowerBounds.1 h _ ⟨fract x - 1, _, by rw [abs_sub_comm, abs_one_sub_fract]⟩⟩
no goals
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ abs (fract x - 1) = 1 - fract x
rw [abs_sub_comm, abs_one_sub_fract]
no goals
case a.refine'_1
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x ∈ {m | ↑m = ↑x}
simp only [mem_setOf, fract, sub_eq_self, QuotientAddGroup.mk_sub,
  QuotientAddGroup.eq_zero_iff, int_cast_mem_zmultiples_one]
no goals
case a.refine'_2
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x - 1 ∈ {m | ↑m = ↑x}
simp only [mem_setOf, fract, sub_eq_self, QuotientAddGroup.mk_sub,
  QuotientAddGroup.eq_zero_iff, int_cast_mem_zmultiples_one, sub_sub,
  (by norm_cast : (⌊x⌋ : ℝ) + 1 = (↑(⌊x⌋ + 1) : ℝ))]
no goals
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ ↑⌊x⌋ + 1 = ↑(⌊x⌋ + 1)
norm_cast
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ ∀ (b : ℝ), b ∈ abs '' {m | ↑m = ↑x} → min (fract x) (1 - fract x) ≤ b
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ min (fract x) (1 - fract x) ≤ sInf (norm '' {m | ↑m = ↑x})
simp only [QuotientAddGroup.mk'_apply, Real.norm_eq_abs, le_csInf_iff h₁ h₂]
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
hb : b ∈ {m | ↑m = ↑x}
⊢ min (fract x) (1 - fract x) ≤ abs b
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
⊢ ∀ (b : ℝ), b ∈ abs '' {m | ↑m = ↑x} → min (fract x) (1 - fract x) ≤ b
rintro b' ⟨b, hb, rfl⟩
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
hb : ∃ k, ↑k = b - x
⊢ min (fract x) (1 - fract x) ≤ abs b
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
hb : b ∈ {m | ↑m = ↑x}
⊢ min (fract x) (1 - fract x) ≤ abs b
simp only [mem_setOf, QuotientAddGroup.eq_iff_sub_mem, mem_zmultiples_iff,
  smul_one_eq_coe] at hb
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ min (fract x) (1 - fract x) ≤ abs b
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
hb : ∃ k, ↑k = b - x
⊢ min (fract x) (1 - fract x) ≤ abs b
obtain ⟨z, hz⟩ := hb
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ abs (b - ↑(round b)) ≤ abs b
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ min (fract x) (1 - fract x) ≤ abs b
rw [(by rw [hz]; abel : x = b - z), fract_sub_int, ← abs_sub_round_eq_min]
case h.e'_4.h.e'_3
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ b = b - ↑0
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ abs (b - ↑(round b)) ≤ abs b
convert round_le b 0
no goals
case h.e'_4.h.e'_3
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ b = b - ↑0
simp
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - (b - x)
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - ↑z
rw [hz]
no goals
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : Set.Nonempty (abs '' {m | ↑m = ↑x})
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - (b - x)
abel