-- Mathlib/Topology/Instances/AddCircle.lean
theorem continuous_right_toIcoMod : ContinuousWithinAt (toIcoMod hp a) (Ici x) x

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 (toIcoMod hp a x)
this : Nontrivial 𝕜
⊢ ∃ u ∈ 𝓝 x, u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s

Tactic:
simp_rw [mem_nhds_iff_exists_Ioo_subset] at h ⊢

Result:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
h : ∃ l u, toIcoMod hp a x ∈ Ioo l u ∧ Ioo l u ⊆ s
⊢ ∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s

Proof state:
case intro.intro.intro.refine_2.intro.a
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ y - ?intro.intro.intro.refine_2.intro.a.m • p ∈ Ioo l u

case intro.intro.intro.refine_2.intro.a
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ y - ?intro.intro.intro.refine_2.intro.a.m • p ∈ Ico a (a + p)

case intro.intro.intro.refine_2.intro.a.m
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ ℤ

case intro.intro.intro.refine_2.intro.a.m
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ ℤ

Tactic:
exacts [⟨h.1, h.2.2⟩, ⟨hd.1.trans (sub_le_sub_right h' _), h.2.1⟩]

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
⊢ l < x - d ∧ x - d < a + p ∧ x - d < u

Tactic:
exact ⟨hxI.1, hd.2, hxI.2⟩

Result:
no goals

Proof state:
case intro.intro.intro.refine_2.intro.a
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ toIcoMod hp a y ∈ Ioo l u

Tactic:
rw [← toIcoMod_sub_zsmul, (toIcoMod_eq_self _).2]

Result:
case intro.intro.intro.refine_2.intro.a
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ y - ?intro.intro.intro.refine_2.intro.a.m • p ∈ Ioo l u

case intro.intro.intro.refine_2.intro.a
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ y - ?intro.intro.intro.refine_2.intro.a.m • p ∈ Ico a (a + p)

case intro.intro.intro.refine_2.intro.a.m
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ ℤ

case intro.intro.intro.refine_2.intro.a.m
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
y : 𝕜
h : l < y - d ∧ y - d < a + p ∧ y - d < u
h' : y ∈ Ici x
⊢ ℤ

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 (toIcoMod hp a x)
⊢ s ∈ Filter.map (toIcoMod hp a) (𝓝[≥] x)

Tactic:
rw [Filter.mem_map, mem_nhdsWithin_iff_exists_mem_nhds_inter]

Result:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 (toIcoMod hp a x)
⊢ ∃ u ∈ 𝓝 x, u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIcoMod hp a) (Ici x) x

Tactic:
intro s h

Result:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 (toIcoMod hp a x)
⊢ s ∈ Filter.map (toIcoMod hp a) (𝓝[≥] x)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
⊢ ∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s

Tactic:
have hd := toIcoMod_mem_Ico hp a x

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
this : Nontrivial 𝕜
l u : 𝕜
hxI : toIcoMod hp a x ∈ Ioo l u
hIs : Ioo l u ⊆ s
d : 𝕜 := toIcoDiv hp a x • p
hd : toIcoMod hp a x ∈ Ico a (a + p)
⊢ ∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s