-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_eq {x : ℝ} : ‖(x : AddCircle p)‖ = |x - round (p⁻¹ * x) * p|

Proof state:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ sInf (norm '' {m | ↑m = ↑x}) = fract x ⊓ (1 - fract x)

Tactic:
apply le_antisymm

Result:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ sInf (norm '' {m | ↑m = ↑x}) ≤ fract x ⊓ (1 - fract x)

case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ fract x ⊓ (1 - fract x) ≤ sInf (norm '' {m | ↑m = ↑x})

Proof state:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p⁻¹| * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx

Result:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Proof state:
case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (0⁻¹ * x)) * 0|

Tactic:
simp

Result:
no goals

Proof state:
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ fract x ⊓ (1 - fract x) ≤ |b|

Tactic:
rw [(by rw [hz]; abel : x = b - z), fract_sub_int, ← abs_sub_round_eq_min]

Result:
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ |b - ↑(round b)| ≤ |b|

Proof state:
⊢ ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|

Tactic:
intros x

Result:
x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|

Proof state:
x : ℝ
⊢ sInf (norm '' {m | ↑m = ↑x}) = fract x ⊓ (1 - fract x)

Tactic:
have h₁ : BddBelow (abs '' { m : ℝ | (m : AddCircle (1 : ℝ)) = x }) :=
  ⟨0, by simp [mem_lowerBounds]⟩

Result:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = fract x ⊓ (1 - fract x)

Proof state:
case h.e'_4.h.e'_4
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ b = b - ↑0

Tactic:
simp

Result:
no goals

Proof state:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ sInf (norm '' {m | ↑m = ↑x}) ≤ fract x ⊓ (1 - fract x)

Tactic:
simp_rw [Real.norm_eq_abs, csInf_le_iff h₁ h₂, le_min_iff]

Result:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ ∀ b ∈ lowerBounds (abs '' {m | ↑m = ↑x}), b ≤ fract x ∧ b ≤ 1 - fract x

Proof state:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - (b - x)

Tactic:
abel

Result:
no goals

Proof state:
case a.refine_1
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x ∈ {m | ↑m = ↑x}

Tactic:
simp only [mem_setOf, fract, sub_eq_self, QuotientAddGroup.mk_sub,
  QuotientAddGroup.eq_zero_iff, intCast_mem_zmultiples_one]

Result:
no goals

Proof state:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑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]

Result:
no goals

Proof state:
p x : ℝ
⊢ ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|

Tactic:
clear! x p

Result:
⊢ ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|

Proof state:
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
hb : ∃ k, ↑k = b - x
⊢ fract x ⊓ (1 - fract x) ≤ |b|

Tactic:
obtain ⟨z, hz⟩ := hb

Result:
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ fract x ⊓ (1 - fract x) ≤ |b|

Proof state:
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
hb : b ∈ {m | ↑m = ↑x}
⊢ fract x ⊓ (1 - fract x) ≤ |b|

Tactic:
simp only [mem_setOf, QuotientAddGroup.eq_iff_sub_mem, mem_zmultiples_iff,
  smul_one_eq_cast] at hb

Result:
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
hb : ∃ k, ↑k = b - x
⊢ fract x ⊓ (1 - fract x) ≤ |b|

Proof state:
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

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

Result:
case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (0⁻¹ * x)) * 0|

case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Proof state:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
have hx := norm_coe_mul p x p⁻¹

Result:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p⁻¹| * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Proof state:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ ∀ b ∈ abs '' {m | ↑m = ↑x}, fract x ⊓ (1 - fract x) ≤ b

Tactic:
rintro b' ⟨b, hb, rfl⟩

Result:
case a.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
hb : b ∈ {m | ↑m = ↑x}
⊢ fract x ⊓ (1 - fract x) ≤ |b|

Proof state:
case a.refine_2
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x - 1 ∈ {m | ↑m = ↑x}

Tactic:
simp only [mem_setOf, fract, sub_eq_self, QuotientAddGroup.mk_sub,
  QuotientAddGroup.eq_zero_iff, intCast_mem_zmultiples_one, sub_sub,
  (by norm_cast : (⌊x⌋ : ℝ) + 1 = (↑(⌊x⌋ + 1) : ℝ))]

Result:
no goals

Proof state:
x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|

Tactic:
rw [quotient_norm_eq, abs_sub_round_eq_min]

Result:
x : ℝ
⊢ sInf (norm '' {m | ↑m = ↑x}) = fract x ⊓ (1 - fract x)

Proof state:
x : ℝ
⊢ 0 ∈ lowerBounds (abs '' {m | ↑m = ↑x})

Tactic:
simp [mem_lowerBounds]

Result:
no goals

Proof state:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ b ≤ fract x ∧ b ≤ 1 - fract x

Tactic:
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]⟩⟩

Result:
case a.refine_1
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
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₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ fract x - 1 ∈ {m | ↑m = ↑x}

Proof state:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ ∀ b ∈ lowerBounds (abs '' {m | ↑m = ↑x}), b ≤ fract x ∧ b ≤ 1 - fract x

Tactic:
intro b h

Result:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ b ≤ fract x ∧ b ≤ 1 - fract x

Proof state:
case a.intro.intro.intro
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ |b - ↑(round b)| ≤ |b|

Tactic:
convert round_le b 0

Result:
case h.e'_4.h.e'_4
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ b = b - ↑0

Proof state:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ ↑⌊x⌋ + 1 = ↑(⌊x⌋ + 1)

Tactic:
norm_cast

Result:
no goals

Proof state:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
⊢ sInf (norm '' {m | ↑m = ↑x}) = fract x ⊓ (1 - fract x)

Tactic:
have h₂ : (abs '' { m : ℝ | (m : AddCircle (1 : ℝ)) = x }).Nonempty := ⟨|x|, ⟨x, rfl, rfl⟩⟩

Result:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ sInf (norm '' {m | ↑m = ↑x}) = fract x ⊓ (1 - fract x)