-- Mathlib/Algebra/Order/Floor.lean
theorem image_fract (s : Set α) : fract '' s = ⋃ m : ℤ, (fun x : α => x - m) '' s ∩ Ico 0 1

Proof state:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑⌊y⌋
h1 : y - ↑⌊y⌋ < 1
⊢ ∃ x ∈ s, fract x = y - ↑⌊y⌋

Tactic:
exact ⟨y, hys, rfl⟩

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
m : ℤ
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑m
h1 : y - ↑m < 1
⊢ ∃ x ∈ s, fract x = y - ↑m

Tactic:
obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩

Result:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑⌊y⌋
h1 : y - ↑⌊y⌋ < 1
⊢ ∃ x ∈ s, fract x = y - ↑⌊y⌋

Proof state:
case h.mp
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, fract x_1 = x) → ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case h.mp.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
y : α
hy : y ∈ s
⊢ ∃ i, (∃ x ∈ s, x - ↑i = fract y) ∧ fract y ∈ Ico 0 1

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

Tactic:
constructor

Result:
case h.mp
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, fract x_1 = x) → ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

case h.mpr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1 ∈ s, fract x_1 = x

Proof state:
case h.mp.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
y : α
hy : y ∈ s
⊢ ∃ i, (∃ x ∈ s, x - ↑i = fract y) ∧ fract y ∈ Ico 0 1

Tactic:
exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩

Result:
no goals

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ x ∈ fract '' s ↔ x ∈ ⋃ m, (fun x => x - ↑m) '' s ∩ Ico 0 1

Tactic:
simp only [mem_image, mem_inter_iff, mem_iUnion]

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, fract x_1 = x) ↔ ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
⊢ fract '' s = ⋃ m, (fun x => x - ↑m) '' s ∩ Ico 0 1

Tactic:
ext x

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ x ∈ fract '' s ↔ x ∈ ⋃ m, (fun x => x - ↑m) '' s ∩ Ico 0 1

Proof state:
case h.mpr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
x : α
⊢ (∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1 ∈ s, fract x_1 = x

Tactic:
rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩

Result:
case h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
s : Set α
m : ℤ
y : α
hys : y ∈ s
h0 : 0 ≤ y - ↑m
h1 : y - ↑m < 1
⊢ ∃ x ∈ s, fract x = y - ↑m