case inl
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

case inr
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
cases' eq_or_ne (fract a) 0 with ha ha
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ fract a = a + 1 - ↑⌈a⌉
case inr
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
right
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ fract a = a + 1 - ↑⌈a⌉
suffices (⌈a⌉ : α) = ⌊a⌋ + 1 by
  rw [this, ← self_sub_fract]
  abel
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ⌈a⌉ = ⌊a⌋ + 1
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1
norm_cast
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a ∧ a ≤ ↑(⌊a⌋ + 1)
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ⌈a⌉ = ⌊a⌋ + 1
rw [ceil_eq_iff]
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a ∧ a ≤ ↑(⌊a⌋ + 1)
refine' ⟨_, _root_.le_of_lt <| by simp⟩
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ 0 < fract a
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a
rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
no goals
case inr.h
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ 0 < fract a
exact ha.symm.lt_of_le (fract_nonneg a)
no goals
case inl
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
exact Or.inl ha
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - (a - fract a + 1)
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - ↑⌈a⌉
rw [this, ← self_sub_fract]
no goals
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - (a - fract a + 1)
abel
no goals
F : Type ?u.229164
α : Type u_1
β : Type ?u.229170
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
ha : fract a ≠ 0
⊢ a < ↑(⌊a⌋ + 1)
simp