case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ {b | toIcoMod hp a b = toIocMod hp a b} = ⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)
ext1
no goals
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)
simp_rw [Set.mem_setOf, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ←
  not_modEq_iff_toIcoMod_eq_toIocMod, modEq_iff_not_forall_mem_Ioo_mod hp, not_forall,
  Classical.not_not]