F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
h : fract a = fract b
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)
unfold fract at h
no goals
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)
rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]
case intro
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a b : α
z : ℤ
hz : a - b = ↑z
⊢ fract a = fract b
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ (∃ z, a - b = ↑z) → fract a = fract b
rintro ⟨z, hz⟩
case intro
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a b : α
z : ℤ
hz : a - b = ↑z
⊢ a - fract b = ↑(z + ⌊b⌋)
case intro
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a b : α
z : ℤ
hz : a - b = ↑z
⊢ fract a = fract b
refine' fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, _⟩
case intro
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a b : α
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋
case intro
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a b : α
z : ℤ
hz : a - b = ↑z
⊢ a - fract b = ↑(z + ⌊b⌋)
rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]
no goals
case intro
F : Type ?u.164824
α : Type u_1
β : Type ?u.164830
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a b : α
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋
exact add_sub_sub_cancel _ _ _