-- Mathlib/Algebra/Order/Round.lean
theorem round_eq (x : α) : round x = ⌊x + 1 / 2⌋

Proof state:
case inr.right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ fract x ≤ 1

Tactic:
linarith [fract_lt_one x]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋

Tactic:
conv_rhs => rw [← fract_add_floor x, add_assoc, add_left_comm, floor_int_add]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x⌋ + ⌊fract x + 1 / 2⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ 2 * fract x < 1 ↔ fract x < 1 / 2

Tactic:
simp only [lt_div_iff₀', two_pos]

Result:
no goals

Proof state:
case inl.right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ fract x + 1 / 2 < 1

Tactic:
linarith

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x ∧ fract x ≤ 1

Tactic:
constructor

Result:
case inr.left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x

case inr.right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ fract x ≤ 1

Proof state:
case inr
α : Type u_2
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⌋

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

Result:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x ∧ fract x ≤ 1

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x⌋ + ⌊fract x + 1 / 2⌋

Tactic:
rw [if_pos hx, self_eq_add_right, floor_eq_iff, cast_zero, zero_add]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < ↑1 + 1

Tactic:
constructor

Result:
case left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2

case right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < ↑1 + 1

Proof state:
case left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2

Tactic:
norm_num

Result:
case left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ 1 ≤ fract x + 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋

Tactic:
rcases lt_or_le (fract x) (1 / 2) with hx | hx

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋

case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋

Proof state:
case inl.left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2

Tactic:
linarith [fract_nonneg x]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋

Tactic:
simp_rw [round, (by simp only [lt_div_iff₀', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ (if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋

Proof state:
case left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ 1 ≤ fract x + 1 / 2

Tactic:
linarith

Result:
no goals

Proof state:
case right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < ↑1 + 1

Tactic:
norm_num

Result:
case right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < 2

Proof state:
case right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ fract x + 1 / 2 < 2

Tactic:
linarith [fract_lt_one x]

Result:
no goals

Proof state:
case inr.left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
this : ⌊fract x + 1 / 2⌋ = 1
⊢ 0 < fract x

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ⌊fract x + 1 / 2⌋ = 1

Tactic:
rw [floor_eq_iff]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : 1 / 2 ≤ fract x
⊢ ↑1 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < ↑1 + 1

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2 ∧ fract x + 1 / 2 < 1

Tactic:
constructor

Result:
case inl.left
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ 0 ≤ fract x + 1 / 2

case inl.right
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
hx : fract x < 1 / 2
⊢ fract x + 1 / 2 < 1