case inl
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s

case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
cases' le_or_lt (|p| / 2) ε with hε hε
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : abs 0 / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs 0 / 2 then closedBall x ε ∩ s else s

case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
case inl
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
rcases eq_or_ne p 0 with (rfl | hp)
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
hp : p ≠ 0
⊢ s ⊆ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
simp only [not_lt.mpr hε, ite_false, inter_eq_right_iff_subset]
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
hp : p ≠ 0
⊢ s ⊆ univ
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
hp : p ≠ 0
⊢ s ⊆ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε
rw [closedBall_eq_univ_of_half_period_le p hp (↑x : ℝ ⧸ zmultiples p) hε, preimage_univ]
no goals
case inl.inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : abs p / 2 ≤ ε
hp : p ≠ 0
⊢ s ⊆ univ
apply subset_univ
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : 0 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs 0 / 2 then closedBall x ε ∩ s else s
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : abs 0 / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs 0 / 2 then closedBall x ε ∩ s else s
simp only [abs_zero, zero_div] at hε
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : 0 ≤ ε
⊢ s ⊆ closedBall x ε
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : 0 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs 0 / 2 then closedBall x ε ∩ s else s
simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div,
  if_false, inter_eq_right_iff_subset]
no goals
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : 0 ≤ ε
⊢ s ⊆ closedBall x ε
exact hs.trans (closedBall_subset_closedBall <| by simp [hε])
no goals
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs 0 / 2)
hε : 0 ≤ ε
⊢ abs 0 / 2 ≤ ε
simp [hε]
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
⊢ ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
suffices ∀ z : ℤ, closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅ by
  simp [-zsmul_eq_mul, ← QuotientAddGroup.mk_zero, coe_real_preimage_closedBall_eq_iUnion,
    iUnion_inter, iUnion_ite, this, hε]
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
⊢ ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
intro z
case inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
simp only [Real.closedBall_eq_Icc, zero_sub, zero_add] at hs⊢
case inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
⊢ Icc (x + 0 • p - ε) (x + 0 • p + ε) ∩ s = if 0 = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
case inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
rcases eq_or_ne z 0 with (rfl | hz)
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
⊢ ∀ (x_1 : ℝ), ¬x_1 ∈ Icc (x + ↑z * p - ε) (x + ↑z * p + ε) ∩ s
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_not_mem]
case inr.inr.intro.intro
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
⊢ False
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
⊢ ∀ (x_1 : ℝ), ¬x_1 ∈ Icc (x + ↑z * p - ε) (x + ↑z * p + ε) ∩ s
rintro y ⟨⟨hy₁, hy₂⟩, hy₀⟩
case inr.inr.intro.intro.intro
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
⊢ False
case inr.inr.intro.intro
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
⊢ False
obtain ⟨hy₃, hy₄⟩ := hs hy₀
case inr.inr.intro.intro.intro.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
⊢ False

case inr.inr.intro.intro.intro.inr.inl
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hε : ε < abs 0 / 2
hs : s ⊆ Icc (x - abs 0 / 2) (x + abs 0 / 2)
hy₁ : x + ↑z * 0 - ε ≤ y
hy₂ : y ≤ x + ↑z * 0 + ε
hy₃ : x - abs 0 / 2 ≤ y
hy₄ : y ≤ x + abs 0 / 2
⊢ False

case inr.inr.intro.intro.intro.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
⊢ False
case inr.inr.intro.intro.intro
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
⊢ False
rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)
no goals
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (abs p / 2)
hε : ε < abs p / 2
this : ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < abs p / 2 then closedBall x ε ∩ s else s
simp [-zsmul_eq_mul, ← QuotientAddGroup.mk_zero, coe_real_preimage_closedBall_eq_iUnion,
  iUnion_inter, iUnion_ite, this, hε]
no goals
case inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
⊢ Icc (x + 0 • p - ε) (x + 0 • p + ε) ∩ s = if 0 = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
simp
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ False

case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False
case inr.inr.intro.intro.intro.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
⊢ False
cases' Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' hz'
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ ↑z * p ≤ -p

case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
this : ↑z * p ≤ -p
⊢ False
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ False
have : ↑z * p ≤ -p
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
this : ↑z * p ≤ -p
⊢ False
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ ↑z * p ≤ -p

case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
this : ↑z * p ≤ -p
⊢ False
nlinarith
no goals
case inr.inr.intro.intro.intro.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : ↑z ≤ -1
this : ↑z * p ≤ -p
⊢ False
linarith [abs_eq_self.mpr hp.le]
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ p ≤ ↑z * p

case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False
have : p ≤ ↑z * p
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ p ≤ ↑z * p

case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
nlinarith
no goals
case inr.inr.intro.intro.intro.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : 0 < p
hz' : 1 ≤ ↑z
this : p ≤ ↑z * p
⊢ False
linarith [abs_eq_self.mpr hp.le]
case inr.inr.intro.intro.intro.inr.inl
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hs : s ⊆ Icc (x - abs 0 / 2) (x + abs 0 / 2)
hy₃ : x - abs 0 / 2 ≤ y
hy₄ : y ≤ x + abs 0 / 2
hy₁ : x - ε ≤ y
hy₂ : y ≤ x + ε
hε : ε < 0
⊢ False
case inr.inr.intro.intro.intro.inr.inl
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hε : ε < abs 0 / 2
hs : s ⊆ Icc (x - abs 0 / 2) (x + abs 0 / 2)
hy₁ : x + ↑z * 0 - ε ≤ y
hy₂ : y ≤ x + ↑z * 0 + ε
hy₃ : x - abs 0 / 2 ≤ y
hy₄ : y ≤ x + abs 0 / 2
⊢ False
simp only [MulZeroClass.mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
no goals
case inr.inr.intro.intro.intro.inr.inl
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hs : s ⊆ Icc (x - abs 0 / 2) (x + abs 0 / 2)
hy₃ : x - abs 0 / 2 ≤ y
hy₄ : y ≤ x + abs 0 / 2
hy₁ : x - ε ≤ y
hy₂ : y ≤ x + ε
hε : ε < 0
⊢ False
linarith
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ False

case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ False
case inr.inr.intro.intro.intro.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
⊢ False
cases' Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' hz'
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ -p ≤ ↑z * p

case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ False
have : -p ≤ ↑z * p
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ -p ≤ ↑z * p

case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
nlinarith
no goals
case inr.inr.intro.intro.intro.inr.inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : ↑z ≤ -1
this : -p ≤ ↑z * p
⊢ False
linarith [abs_eq_neg_self.mpr hp.le]
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ ↑z * p ≤ p

case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ False
have : ↑z * p ≤ p
case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
case this
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ ↑z * p ≤ p

case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
nlinarith
no goals
case inr.inr.intro.intro.intro.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < abs p / 2
z : ℤ
hs : s ⊆ Icc (x - abs p / 2) (x + abs p / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - abs p / 2 ≤ y
hy₄ : y ≤ x + abs p / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
linarith [abs_eq_neg_self.mpr hp.le]