case h
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
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.180856
α : Type u_1
β : Type ?u.180862
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.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ fract x_1 = x) ↔ ∃ i, (∃ x_1, x_1 ∈ s ∧ x_1 - ↑i = x) ∧ x ∈ Ico 0 1
case h
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
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_image, mem_inter_iff, mem_iUnion]
case h.mp
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ fract x_1 = x) → ∃ i, (∃ x_1, x_1 ∈ s ∧ x_1 - ↑i = x) ∧ x ∈ Ico 0 1

case h.mpr
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ i, (∃ x_1, x_1 ∈ s ∧ x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1, x_1 ∈ s ∧ fract x_1 = x
case h
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ fract x_1 = x) ↔ ∃ i, (∃ x_1, x_1 ∈ s ∧ x_1 - ↑i = x) ∧ x ∈ Ico 0 1
constructor
case h.mp.intro.intro
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
y : α
hy : y ∈ s
⊢ ∃ i, (∃ x, x ∈ s ∧ x - ↑i = fract y) ∧ fract y ∈ Ico 0 1
case h.mp
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ fract x_1 = x) → ∃ i, (∃ x_1, x_1 ∈ s ∧ x_1 - ↑i = x) ∧ x ∈ Ico 0 1
rintro ⟨y, hy, rfl⟩
no goals
case h.mp.intro.intro
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
y : α
hy : y ∈ s
⊢ ∃ i, (∃ x, x ∈ s ∧ x - ↑i = fract y) ∧ fract y ∈ Ico 0 1
exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩
case h.mpr.intro.intro.intro.intro.intro
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
m : ℤ
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑m
h1 : y - ↑m < 1
⊢ ∃ x, x ∈ s ∧ fract x = y - ↑m
case h.mpr
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
x : α
⊢ (∃ i, (∃ x_1, x_1 ∈ s ∧ x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1, x_1 ∈ s ∧ fract x_1 = x
rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩
case h.mpr.intro.intro.intro.intro.intro
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑⌊y⌋
h1 : y - ↑⌊y⌋ < 1
⊢ ∃ x, x ∈ s ∧ fract x = y - ↑⌊y⌋
case h.mpr.intro.intro.intro.intro.intro
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
m : ℤ
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑m
h1 : y - ↑m < 1
⊢ ∃ x, x ∈ s ∧ fract x = y - ↑m
obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩
no goals
case h.mpr.intro.intro.intro.intro.intro
F : Type ?u.180856
α : Type u_1
β : Type ?u.180862
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
s : Set α
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑⌊y⌋
h1 : y - ↑⌊y⌋ < 1
⊢ ∃ x, x ∈ s ∧ fract x = y - ↑⌊y⌋
exact ⟨y, hys, rfl⟩