-- Mathlib/Algebra/Order/Floor.lean
theorem fract_eq_zero_or_add_one_sub_ceil (a : α) : fract a = 0 ∨ fract a = a + 1 - (⌈a⌉ : α)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ a < ↑(⌊a⌋ + 1)

Tactic:
simp

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a ∧ a ≤ ↑(⌊a⌋ + 1)

Tactic:
refine ⟨?_, _root_.le_of_lt <| by simp⟩

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
exact Or.inl ha

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
suffices (⌈a⌉ : α) = ⌊a⌋ + 1 by
  rw [this, ← self_sub_fract]
  abel

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
rw [this, ← self_sub_fract]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - (a - fract a + 1)

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1

Tactic:
norm_cast

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ⌈a⌉ = ⌊a⌋ + 1

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
right

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ fract a = a + 1 - ↑⌈a⌉

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a

Tactic:
rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ 0 < fract a

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ 0 < fract a

Tactic:
exact ha.symm.lt_of_le (fract_nonneg a)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - (a - fract a + 1)

Tactic:
abel

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ⌈a⌉ = ⌊a⌋ + 1

Tactic:
rw [ceil_eq_iff]

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a ∧ a ≤ ↑(⌊a⌋ + 1)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
rcases eq_or_ne (fract a) 0 with ha | ha

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

case inr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉