F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋
simp_rw [round, (by simp only [lt_div_iff', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)]
case inl
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋

case inr
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
cases' lt_or_le (fract x) (1 / 2) with hx hx
no goals
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ 2 * fract x < 1 ↔ fract x < 1 / 2
simp only [lt_div_iff', two_pos]
case inl
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x⌋ + ⌊fract x + 1 / 2⌋
case inl
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
conv_rhs => rw [← fract_add_floor x, add_assoc, add_left_comm, floor_int_add]
case inl
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < 1
case inl
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x⌋ + ⌊fract x + 1 / 2⌋
rw [if_pos hx, self_eq_add_right, floor_eq_iff, cast_zero, zero_add]
case inl.left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2

case inl.right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ fract x + 1 / 2 < 1
case inl
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < 1
constructor
no goals
case inl.left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2
linarith [fract_nonneg x]
no goals
case inl.right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ fract x + 1 / 2 < 1
linarith
case inr
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x ∧ fract x ≤ 1
case inr
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
rw [if_neg (not_lt.mpr hx), ← fract_add_floor x, add_assoc, add_left_comm, floor_int_add,
  ceil_add_int, add_comm _ ⌊x⌋, add_right_inj, ceil_eq_iff, this, cast_one, sub_self]
case inr.left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x

case inr.right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ fract x ≤ 1
case inr
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x ∧ fract x ≤ 1
constructor
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < ↑1 + 1
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ⌊fract x + 1 / 2⌋ = 1
rw [floor_eq_iff]
case left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2

case right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < ↑1 + 1
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < ↑1 + 1
constructor
case left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ 1 ≤ fract x + 1 / 2
case left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2
norm_num
no goals
case left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ 1 ≤ fract x + 1 / 2
linarith
case right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < 2
case right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < ↑1 + 1
norm_num
no goals
case right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < 2
linarith [fract_lt_one x]
no goals
case inr.left
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x
linarith
no goals
case inr.right
F : Type ?u.270515
α : Type u_1
β : Type ?u.270521
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ fract x ≤ 1
linarith [fract_lt_one x]