case h
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ x ∈ fract ⁻¹' s ↔ x ∈ ⋃ (m : ℤ), (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
⊢ fract ⁻¹' s = ⋃ (m : ℤ), (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)
ext x
case h
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1
case h
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ x ∈ fract ⁻¹' s ↔ x ∈ ⋃ (m : ℤ), (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)
simp only [mem_preimage, mem_iUnion, mem_inter_iff]
case h
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1) → fract x ∈ s
case h
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1
refine' ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, _⟩
case h.intro.intro.intro
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
m : ℤ
hms : x - ↑m ∈ s
hm0 : 0 ≤ x - ↑m
hm1 : x - ↑m < 1
⊢ fract x ∈ s
case h
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1) → fract x ∈ s
rintro ⟨m, hms, hm0, hm1⟩
case h.intro.intro.intro
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
hms : x - ↑⌊x⌋ ∈ s
hm0 : 0 ≤ x - ↑⌊x⌋
hm1 : x - ↑⌊x⌋ < 1
⊢ fract x ∈ s
case h.intro.intro.intro
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
m : ℤ
hms : x - ↑m ∈ s
hm0 : 0 ≤ x - ↑m
hm1 : x - ↑m < 1
⊢ fract x ∈ s
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
no goals
case h.intro.intro.intro
F : Type ?u.178920
α : Type u_1
β : Type ?u.178926
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
hms : x - ↑⌊x⌋ ∈ s
hm0 : 0 ≤ x - ↑⌊x⌋
hm1 : x - ↑⌊x⌋ < 1
⊢ fract x ∈ s
exact hms