F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ abs (x - ↑(round x)) = min (fract x) (1 - fract x)
simp_rw [round, min_def_lt, two_mul, ← lt_tsub_iff_left]
case inl
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x

case inr
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
cases' lt_or_ge (fract x) (1 - fract x) with hx hx
no goals
case inl
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]
case inr
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
this : 0 < fract x
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
case inr
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
have : 0 < fract x := by
  replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
  simpa only [← two_mul, zero_lt_mul_left, zero_lt_two] using hx
no goals
case inr
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
this : 0 < fract x
⊢ abs (x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)) = if fract x < 1 - fract x then fract x else 1 - fract x
rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
  abs_one_sub_fract]
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
⊢ 0 < fract x
replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
no goals
F : Type ?u.259084
α : Type u_1
β : Type ?u.259090
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x
simpa only [← two_mul, zero_lt_mul_left, zero_lt_two] using hx