[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIcoMod hp a) (Ici x) x
[PROOFSTEP]
intro s h
[GOAL]
𝕜 : Type u_1
B : Type u_2
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) (𝓝[Ici x] x)
[PROOFSTEP]
rw [Filter.mem_map, mem_nhdsWithin_iff_exists_mem_nhds_inter]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 (toIcoMod hp a x)
⊢ ∃ u, u ∈ 𝓝 x ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
haveI : Nontrivial 𝕜 := ⟨⟨0, p, hp.ne⟩⟩
[GOAL]
𝕜 : Type u_1
B : Type u_2
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, u ∈ 𝓝 x ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
simp_rw [mem_nhds_iff_exists_Ioo_subset] at h ⊢
[GOAL]
𝕜 : Type u_1
B : Type u_2
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
[PROOFSTEP]
obtain ⟨l, u, hxI, hIs⟩ := h
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
B : Type u_2
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
⊢ ∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
let d := toIcoDiv hp a x • p
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
B : Type u_2
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
[PROOFSTEP]
have hd := toIcoMod_mem_Ico hp a x
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
B : Type u_2
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
[PROOFSTEP]
simp_rw [subset_def, mem_inter_iff]
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
B : Type u_2
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 ∧ ∀ (x : 𝕜), x ∈ Ioo l u_1 → x ∈ u) ∧
      ∀ (x_1 : 𝕜), x_1 ∈ u ∧ x_1 ∈ Ici x → x_1 ∈ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
refine' ⟨_, ⟨l + d, min (a + p) u + d, _, fun x => id⟩, fun y => _⟩
[GOAL]
case intro.intro.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
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)
⊢ x ∈ Ioo (l + d) (min (a + p) u + d)
[PROOFSTEP]
simp_rw [← sub_mem_Ioo_iff_left, mem_Ioo, lt_min_iff]
[GOAL]
case intro.intro.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
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 : 𝕜
⊢ y ∈ Ioo (l + d) (min (a + p) u + d) ∧ y ∈ Ici x → y ∈ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
simp_rw [← sub_mem_Ioo_iff_left, mem_Ioo, lt_min_iff]
[GOAL]
case intro.intro.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
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 - toIcoDiv hp a x • p ∧ x - toIcoDiv hp a x • p < a + p ∧ x - toIcoDiv hp a x • p < u
[PROOFSTEP]
exact ⟨hxI.1, hd.2, hxI.2⟩
[GOAL]
case intro.intro.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
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 : 𝕜
⊢ (l < y - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < u) ∧ y ∈ Ici x →
    y ∈ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
rintro ⟨h, h'⟩
[GOAL]
case intro.intro.intro.refine'_2.intro
𝕜 : Type u_1
B : Type u_2
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 - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < u
h' : y ∈ Ici x
⊢ y ∈ toIcoMod hp a ⁻¹' s
[PROOFSTEP]
apply hIs
[GOAL]
case intro.intro.intro.refine'_2.intro.a
𝕜 : Type u_1
B : Type u_2
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 - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < u
h' : y ∈ Ici x
⊢ toIcoMod hp a y ∈ Ioo l u
[PROOFSTEP]
rw [← toIcoMod_sub_zsmul, (toIcoMod_eq_self _).2]
[GOAL]
case intro.intro.intro.refine'_2.intro.a
𝕜 : Type u_1
B : Type u_2
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 - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < 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
B : Type u_2
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 - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < 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
B : Type u_2
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 - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < u
h' : y ∈ Ici x
⊢ ℤ
case intro.intro.intro.refine'_2.intro.a.m
𝕜 : Type u_1
B : Type u_2
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 - toIcoDiv hp a x • p ∧ y - toIcoDiv hp a x • p < a + p ∧ y - toIcoDiv hp a x • p < u
h' : y ∈ Ici x
⊢ ℤ
[PROOFSTEP]
exacts [⟨h.1, h.2.2⟩, ⟨hd.1.trans (sub_le_sub_right h' _), h.2.1⟩]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIocMod hp a) (Iic x) x
[PROOFSTEP]
rw [(funext fun y => Eq.trans (by rw [neg_neg]) <| toIocMod_neg _ _ _ :
    toIocMod hp a = (fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg)]
  -- Porting note: added
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x y : 𝕜
⊢ toIocMod hp a y = toIocMod hp a (- -y)
[PROOFSTEP]
rw [neg_neg]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
[PROOFSTEP]
have : ContinuousNeg 𝕜 := TopologicalAddGroup.toContinuousNeg
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
this : ContinuousNeg 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
[PROOFSTEP]
exact
  (continuous_sub_left _).continuousAt.comp_continuousWithinAt <|
    (continuous_right_toIcoMod _ _ _).comp continuous_neg.continuousWithinAt fun y => neg_le_neg
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen {x | (fun x => toIcoMod hp a x = toIocMod hp a x) x}
[PROOFSTEP]
rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))
[PROOFSTEP]
exact isOpen_iUnion fun i => isOpen_Ioo
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p x : 𝕜
⊢ ↑x = 0 ↔ ∃ n, n • p = x
[PROOFSTEP]
simp [AddSubgroup.mem_zmultiples_iff]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ ↑x = 0 ↔ ∃ n, n • p = x
[PROOFSTEP]
rw [coe_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) → ∃ n, n • p = x
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mpr
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) → ∃ n, n • p = x
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mp.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
[PROOFSTEP]
replace hx : 0 < n
[GOAL]
case hx
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 0 < n
[PROOFSTEP]
contrapose! hx
[GOAL]
case hx
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0
[PROOFSTEP]
simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)
[GOAL]
case mp.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ∃ n_1, n_1 • p = n • p
[PROOFSTEP]
exact ⟨n.toNat, by rw [← coe_nat_zsmul, Int.toNat_of_nonneg hx.le]⟩
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ Int.toNat n • p = n • p
[PROOFSTEP]
rw [← coe_nat_zsmul, Int.toNat_of_nonneg hx.le]
[GOAL]
case mpr.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
[PROOFSTEP]
exact ⟨(n : ℤ), by simp⟩
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ↑n • p = n • p
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p x : 𝕜
⊢ ↑(x + p) = ↑x
[PROOFSTEP]
rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ ↑x = ↑y ↔ x = y
[PROOFSTEP]
refine' ⟨fun h => _, by tauto⟩
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ x = y → ↑x = ↑y
[PROOFSTEP]
tauto
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ x = y
[PROOFSTEP]
suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
this : { val := x, property := hx } = { val := y, property := hy }
⊢ x = y
[PROOFSTEP]
exact Subtype.mk.inj this
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
apply_fun equivIco p a at h 
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑(equivIco p a) ↑x = ↑(equivIco p a) ↑y
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑(equivIco p a) ↑x = ↑(equivIco p a) ↑y
⊢ Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) { val := x, property := hx }) =
    Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) { val := y, property := hy })
[PROOFSTEP]
exact h
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIco p a f ↑x = f x
[PROOFSTEP]
have : (equivIco p a) x = ⟨x, hx⟩ := by
  rw [Equiv.apply_eq_iff_eq_symm_apply]
  rfl
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑(equivIco p a) ↑x = { val := x, property := hx }
[PROOFSTEP]
rw [Equiv.apply_eq_iff_eq_symm_apply]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = ↑(equivIco p a).symm { val := x, property := hx }
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : ↑(equivIco p a) ↑x = { val := x, property := hx }
⊢ liftIco p a f ↑x = f x
[PROOFSTEP]
rw [liftIco, comp_apply, this]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : ↑(equivIco p a) ↑x = { val := x, property := hx }
⊢ restrict (Ico a (a + p)) f { val := x, property := hx } = f x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ liftIoc p a f ↑x = f x
[PROOFSTEP]
have : (equivIoc p a) x = ⟨x, hx⟩ := by
  rw [Equiv.apply_eq_iff_eq_symm_apply]
  rfl
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ ↑(equivIoc p a) ↑x = { val := x, property := hx }
[PROOFSTEP]
rw [Equiv.apply_eq_iff_eq_symm_apply]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ ↑x = ↑(equivIoc p a).symm { val := x, property := hx }
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
this : ↑(equivIoc p a) ↑x = { val := x, property := hx }
⊢ liftIoc p a f ↑x = f x
[PROOFSTEP]
rw [liftIoc, comp_apply, this]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
this : ↑(equivIoc p a) ↑x = { val := x, property := hx }
⊢ restrict (Ioc a (a + p)) f { val := x, property := hx } = f x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (↑(equivIco p a)) x
[PROOFSTEP]
induction x using QuotientAddGroup.induction_on'
[GOAL]
case H
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ↑(equivIco p a) ↑z✝
[PROOFSTEP]
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
[GOAL]
case H
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (↑(equivIco p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 (↑(equivIco p a) ↑z✝)
[PROOFSTEP]
exact (continuousAt_toIcoMod hp.out a hx).codRestrict _
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (↑(equivIoc p a)) x
[PROOFSTEP]
induction x using QuotientAddGroup.induction_on'
[GOAL]
case H
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ↑(equivIoc p a) ↑z✝
[PROOFSTEP]
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
[GOAL]
case H
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (↑(equivIoc p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 (↑(equivIoc p a) ↑z✝)
[PROOFSTEP]
exact (continuousAt_toIocMod hp.out a hx).codRestrict _
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ QuotientAddGroup.mk '' Ico a (a + p) = univ
[PROOFSTEP]
rw [image_eq_range]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x => ↑↑x) = univ
[PROOFSTEP]
exact (equivIco p a).symm.range_eq_univ
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ QuotientAddGroup.mk '' Ioc a (a + p) = univ
[PROOFSTEP]
rw [image_eq_range]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x => ↑↑x) = univ
[PROOFSTEP]
exact (equivIoc p a).symm.range_eq_univ
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ map (↑(AddAut.mulRight ((Units.mk0 p hp)⁻¹ * Units.mk0 q hq))) (zmultiples p) = zmultiples q
[PROOFSTEP]
rw [AddMonoidHom.map_zmultiples, AddMonoidHom.coe_coe, AddAut.mulRight_apply, Units.val_mul, Units.val_mk0,
  Units.val_inv_eq_inv_val, Units.val_mk0, mul_inv_cancel_left₀ hp]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
x : AddCircle p
⊢ (fun x n => ↑((↑n)⁻¹ * ↑(↑(equivIco p 0) x))) x 0 = 0
[PROOFSTEP]
simp only [algebraMap.coe_zero, Int.cast_zero, inv_zero, zero_mul, QuotientAddGroup.mk_zero]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : n ≠ 0
⊢ n • (fun x n => ↑((↑n)⁻¹ * ↑(↑(equivIco p 0) x))) x n = x
[PROOFSTEP]
replace hn : (n : 𝕜) ≠ 0
[GOAL]
case hn
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : ↑n ≠ 0
⊢ n • (fun x n => ↑((↑n)⁻¹ * ↑(↑(equivIco p 0) x))) x n = x
[PROOFSTEP]
change n • QuotientAddGroup.mk' _ ((n : 𝕜)⁻¹ * ↑(equivIco p 0 x)) = x
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : ↑n ≠ 0
⊢ n • ↑(QuotientAddGroup.mk' (zmultiples p)) ((↑n)⁻¹ * ↑(↑(equivIco p 0) x)) = x
[PROOFSTEP]
rw [← map_zsmul, ← smul_mul_assoc, zsmul_eq_mul, mul_inv_cancel hn, one_mul]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : ↑n ≠ 0
⊢ ↑(QuotientAddGroup.mk' (zmultiples p)) ↑(↑(equivIco p 0) x) = x
[PROOFSTEP]
exact (equivIco p 0).symm_apply_apply x
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ addOrderOf ↑(p / ↑n) = n
[PROOFSTEP]
rw [addOrderOf_eq_iff h]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ (m : ℕ), m < n → 0 < m → m • ↑(p / ↑n) ≠ 0
[PROOFSTEP]
replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ n • ↑(p / ↑n) = 0 ∧ ∀ (m : ℕ), m < n → 0 < m → m • ↑(p / ↑n) ≠ 0
[PROOFSTEP]
refine' ⟨_, fun m hn h0 => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ n • ↑(p / ↑n) = 0
[PROOFSTEP]
simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ m • ↑(p / ↑n) ≠ 0
[PROOFSTEP]
simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
[GOAL]
case refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ ↑(↑n * (p / ↑n)) = 0
[PROOFSTEP]
rw [mul_div_cancel' _ h.ne', coe_period]
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬↑(↑m * (p / ↑n)) = 0
[PROOFSTEP]
rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬∃ n_1, n_1 • p = ↑m * (p / ↑n)
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : k • p = ↑m * (p / ↑n)
⊢ False
[PROOFSTEP]
rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul, (mul_left_injective₀ hp.out.ne').eq_iff,
  Nat.cast_inj, mul_comm] at hk 
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : n * k = m
⊢ False
[PROOFSTEP]
exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_lt hn
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd m n * addOrderOf ↑(↑m / ↑n * p) = n
[PROOFSTEP]
rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul, addOrderOf_nsmul'']
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd m n * (addOrderOf ↑(p / ↑n) / Nat.gcd (addOrderOf ↑(p / ↑n)) m) = n
[PROOFSTEP]
rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd n m ∣ n
[PROOFSTEP]
exact n.gcd_dvd_left m
[GOAL]
case h
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)
[PROOFSTEP]
rw [← addOrderOf_pos_iff, addOrderOf_period_div hn]
[GOAL]
case h
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ 0 < n
[PROOFSTEP]
exact hn
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
[PROOFSTEP]
convert gcd_mul_addOrderOf_div_eq p m hn
[GOAL]
case h.e'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = Nat.gcd m n * addOrderOf ↑(↑m / ↑n * p)
[PROOFSTEP]
rw [h, one_mul]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m : ℤ
n : ℕ
hn : 0 < n
h : Nat.gcd (Int.natAbs m) n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
[PROOFSTEP]
induction m
[GOAL]
case ofNat
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.ofNat a✝)) n = 1
⊢ addOrderOf ↑(↑(Int.ofNat a✝) / ↑n * p) = n
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, Int.cast_ofNat, Int.natAbs_ofNat] at h ⊢
[GOAL]
case ofNat
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd a✝ n = 1
⊢ addOrderOf ↑(↑a✝ / ↑n * p) = n
[PROOFSTEP]
exact addOrderOf_div_of_gcd_eq_one hn h
[GOAL]
case negSucc
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.negSucc a✝)) n = 1
⊢ addOrderOf ↑(↑(Int.negSucc a✝) / ↑n * p) = n
[PROOFSTEP]
simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]
[GOAL]
case negSucc
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : Nat.gcd (Int.natAbs (Int.negSucc a✝)) n = 1
⊢ addOrderOf ↑(↑(a✝ + 1) / ↑n * p) = n
[PROOFSTEP]
exact addOrderOf_div_of_gcd_eq_one hn h
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ addOrderOf ↑(↑q * p) = q.den
[PROOFSTEP]
have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
  norm_cast
  exact q.pos.ne.symm
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ↑↑q.den ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ¬q.den = 0
[PROOFSTEP]
exact q.pos.ne.symm
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q * p) = q.den
[PROOFSTEP]
rw [← @Rat.num_den q, Rat.cast_mk_of_ne_zero _ _ this, Int.cast_ofNat, Rat.num_den,
  addOrderOf_div_of_gcd_eq_one' q.pos q.reduced]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = u
[PROOFSTEP]
refine' ⟨QuotientAddGroup.induction_on' u fun k hk => _, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n
[PROOFSTEP]
rintro ⟨m, _, h₁, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
left✝ : m < n
h₁ : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
[PROOFSTEP]
exact addOrderOf_div_of_gcd_eq_one h h₁
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
have h0 := addOrderOf_nsmul_eq_zero (k : AddCircle p)
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : addOrderOf ↑k • ↑k = 0
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
rw [hk, ← coe_nsmul, coe_eq_zero_iff] at h0 
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
h0 : ∃ n_1, n_1 • p = n • k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
obtain ⟨a, ha⟩ := h0
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
have h0 : (_ : 𝕜) ≠ 0 := Nat.cast_ne_zero.2 h.ne'
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : a • p = n • k
h0 : ↑n ≠ 0
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.ediv_add_emod' n, add_smul, add_div, zsmul_eq_mul, Int.cast_mul,
  Int.cast_ofNat, mul_assoc, ← mul_div, mul_comm _ p, mul_div_cancel p h0] at ha 
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
have han : _ = a % n := Int.toNat_of_nonneg (Int.emod_nonneg _ <| by exact_mod_cast h.ne')
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast h.ne'
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
have he : (↑(↑((a % n).toNat) / ↑n * p) : AddCircle p) = k
[GOAL]
case he
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
[PROOFSTEP]
convert congr_arg (QuotientAddGroup.mk : 𝕜 → (AddCircle p)) ha using 1
[GOAL]
case h.e'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
⊢ ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑(↑(a / ↑n) * p + (a % ↑n) • p / ↑n)
[PROOFSTEP]
rw [coe_add, ← Int.cast_ofNat, han, zsmul_eq_mul, mul_div_right_comm, eq_comm, add_left_eq_self, ← zsmul_eq_mul,
  coe_zsmul, coe_period, smul_zero]
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ ∃ m, m < n ∧ Nat.gcd m n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
[PROOFSTEP]
refine' ⟨(a % n).toNat, _, _, he⟩
[GOAL]
case refine'_2.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ Int.toNat (a % ↑n) < n
[PROOFSTEP]
rw [← Int.ofNat_lt, han]
[GOAL]
case refine'_2.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ a % ↑n < ↑n
[PROOFSTEP]
exact Int.emod_lt_of_pos _ (Int.ofNat_lt.2 h)
[GOAL]
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
[PROOFSTEP]
have := (gcd_mul_addOrderOf_div_eq p (Int.toNat (a % ↑n)) h).trans ((congr_arg addOrderOf he).trans hk).symm
[GOAL]
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this :
  Nat.gcd (Int.toNat (a % ↑n)) n * addOrderOf ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) =
    addOrderOf ↑(↑(Int.toNat (a % ↑n)) / ↑n * p)
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
[PROOFSTEP]
rw [he, Nat.mul_left_eq_self_iff] at this 
[GOAL]
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this : Nat.gcd (Int.toNat (a % ↑n)) n = 1
⊢ Nat.gcd (Int.toNat (a % ↑n)) n = 1
[PROOFSTEP]
exact this
[GOAL]
case refine'_2.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : addOrderOf ↑k = n
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
han : ↑(Int.toNat (a % ↑n)) = a % ↑n
he : ↑(↑(Int.toNat (a % ↑n)) / ↑n * p) = ↑k
this : Nat.gcd (Int.toNat (a % ↑n)) n * addOrderOf ↑k = addOrderOf ↑k
⊢ 0 < addOrderOf ↑k
[PROOFSTEP]
rwa [hk]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Bijective fun m => { val := ↑(↑↑m / ↑n * p), property := (_ : addOrderOf ↑(↑↑m / ↑n * p) = n) }
[PROOFSTEP]
refine' ⟨fun m₁ m₂ h => Subtype.ext _, fun u => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h :
  (fun m => { val := ↑(↑↑m / ↑n * p), property := (_ : addOrderOf ↑(↑↑m / ↑n * p) = n) }) m₁ =
    (fun m => { val := ↑(↑↑m / ↑n * p), property := (_ : addOrderOf ↑(↑↑m / ↑n * p) = n) }) m₂
⊢ ↑m₁ = ↑m₂
[PROOFSTEP]
simp_rw [Subtype.ext_iff] at h 
[GOAL]
case refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
⊢ ↑m₁ = ↑m₂
[PROOFSTEP]
rw [← sub_eq_zero, ← coe_sub, ← sub_mul, ← sub_div, ← Int.cast_ofNat m₁, ← Int.cast_ofNat m₂, ← Int.cast_sub,
  coe_eq_zero_iff] at h 
[GOAL]
case refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h✝ : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
h : ∃ n_1, n_1 • p = ↑(↑↑m₁ - ↑↑m₂) / ↑n * p
⊢ ↑m₁ = ↑m₂
[PROOFSTEP]
obtain ⟨m, hm⟩ := h
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : m • p = ↑(↑↑m₁ - ↑↑m₂) / ↑n * p
⊢ ↑m₁ = ↑m₂
[PROOFSTEP]
rw [← mul_div_right_comm, eq_div_iff, mul_comm, ← zsmul_eq_mul, mul_smul_comm, ← nsmul_eq_mul, ← coe_nat_zsmul,
  smul_smul, (zsmul_strictMono_left hp.out).injective.eq_iff, mul_comm] at hm 
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑m₁ = ↑m₂
case refine'_1.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : m • p = ↑(↑↑m₁ - ↑↑m₂) * p / ↑n
⊢ ↑n ≠ 0
[PROOFSTEP]
swap
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : m • p = ↑(↑↑m₁ - ↑↑m₂) * p / ↑n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.2 hn.ne'
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑m₁ = ↑m₂
[PROOFSTEP]
rw [← @Nat.cast_inj ℤ, ← sub_eq_zero]
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑↑m₁ - ↑↑m₂ = 0
[PROOFSTEP]
refine' Int.eq_zero_of_abs_lt_dvd ⟨_, hm.symm⟩ (abs_sub_lt_iff.2 ⟨_, _⟩)
[GOAL]
case refine'_1.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑↑m₁ - ↑↑m₂ < ↑n
[PROOFSTEP]
apply (Int.sub_le_self _ <| Nat.cast_nonneg _).trans_lt (Nat.cast_lt.2 _)
[GOAL]
case refine'_1.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑↑m₂ - ↑↑m₁ < ↑n
[PROOFSTEP]
apply (Int.sub_le_self _ <| Nat.cast_nonneg _).trans_lt (Nat.cast_lt.2 _)
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑m₁ < n
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ Nat.gcd m n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
m : ℤ
hm : ↑n * m = ↑↑m₁ - ↑↑m₂
⊢ ↑m₂ < n
[PROOFSTEP]
exacts [m₁.2.1, m₂.2.1]
[GOAL]
case refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m => { val := ↑(↑↑m / ↑n * p), property := (_ : addOrderOf ↑(↑↑m / ↑n * p) = n) }) a = u
[PROOFSTEP]
obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
m : ℕ
hmn : m < n
hg : Nat.gcd m n = 1
he : ↑(↑m / ↑n * p) = ↑u
⊢ ∃ a, (fun m => { val := ↑(↑↑m / ↑n * p), property := (_ : addOrderOf ↑(↑↑m / ↑n * p) = n) }) a = u
[PROOFSTEP]
exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
⊢ Nat.card { u // addOrderOf u = n } = Nat.totient n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0
[PROOFSTEP]
simp only [Nat.totient_zero, addOrderOf_eq_zero_iff]
[GOAL]
case inl
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
[PROOFSTEP]
rcases em (∃ u : AddCircle p, ¬IsOfFinAddOrder u) with (⟨u, hu⟩ | h)
[GOAL]
case inl.inl.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
[PROOFSTEP]
have : Infinite { u : AddCircle p // ¬IsOfFinAddOrder u } :=
  by
  erw [infinite_coe_iff]
  exact infinite_not_isOfFinAddOrder hu
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Infinite { u // ¬IsOfFinAddOrder u }
[PROOFSTEP]
erw [infinite_coe_iff]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite fun u => IsOfFinAddOrder u → False
[PROOFSTEP]
exact infinite_not_isOfFinAddOrder hu
[GOAL]
case inl.inl.intro
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
[PROOFSTEP]
exact Nat.card_eq_zero_of_infinite
[GOAL]
case inl.inr
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
[PROOFSTEP]
have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa using h
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ IsEmpty { u // ¬IsOfFinAddOrder u }
[PROOFSTEP]
simpa using h
[GOAL]
case inl.inr
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
[PROOFSTEP]
exact Nat.card_of_isEmpty
[GOAL]
case inr
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = Nat.totient n
[PROOFSTEP]
rw [← coe_setOf, Nat.card_congr (setAddOrderOfEquiv p hn), n.totient_eq_card_lt_and_coprime]
[GOAL]
case inr
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ Nat.gcd m n = 1} = Nat.card ↑{m | m < n ∧ Nat.coprime n m}
[PROOFSTEP]
simp only [Nat.gcd_comm]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Nat.card ↑{u | addOrderOf u = n} ≠ 0
[PROOFSTEP]
simpa only [coe_setOf, card_addOrderOf_eq_totient p] using (Nat.totient_pos hn).ne'
[GOAL]
𝕜 : Type u_1
B : Type u_2
p : ℝ
inst✝ : Fact (0 < p)
⊢ CompactSpace (AddCircle p)
[PROOFSTEP]
rw [← isCompact_univ_iff, ← coe_image_Icc_eq p 0]
[GOAL]
𝕜 : Type u_1
B : Type u_2
p : ℝ
inst✝ : Fact (0 < p)
⊢ IsCompact (QuotientAddGroup.mk '' Icc 0 (0 + p))
[PROOFSTEP]
exact isCompact_Icc.image (AddCircle.continuous_mk' p)
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : Quot (EndpointIdent p a)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (fun x => ↑↑x) a_1 = (fun x => ↑↑x) b
[PROOFSTEP]
rintro _ _ ⟨_⟩
[GOAL]
case mk
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : Quot (EndpointIdent p a)
⊢ (fun x => ↑↑x) { val := a, property := (_ : a ∈ Icc a (a + p)) } =
    (fun x => ↑↑x) { val := a + p, property := (_ : a + p ∈ Icc a (a + p)) }
[PROOFSTEP]
exact (coe_add_period p a).symm
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (a_1 : ↑(Icc a (a + p))),
    (fun x => Quot.mk (EndpointIdent p a) (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p)) (↑(equivIco p a) x)))
        ((fun x =>
            Quot.liftOn x (fun x => ↑↑x)
              (_ : ∀ (a_2 b : ↑(Icc a (a + p))), EndpointIdent p a a_2 b → (fun x => ↑↑x) a_2 = (fun x => ↑↑x) b))
          (Quot.mk (EndpointIdent p a) a_1)) =
      Quot.mk (EndpointIdent p a) a_1
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
⊢ (fun x => Quot.mk (EndpointIdent p a) (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p)) (↑(equivIco p a) x)))
      ((fun x =>
          Quot.liftOn x (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (fun x => ↑↑x) a_1 = (fun x => ↑↑x) b))
        (Quot.mk (EndpointIdent p a) { val := x, property := hx })) =
    Quot.mk (EndpointIdent p a) { val := x, property := hx }
[PROOFSTEP]
rcases ne_or_eq x (a + p) with (h | rfl)
[GOAL]
case mk.inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ (fun x => Quot.mk (EndpointIdent p a) (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p)) (↑(equivIco p a) x)))
      ((fun x =>
          Quot.liftOn x (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (fun x => ↑↑x) a_1 = (fun x => ↑↑x) b))
        (Quot.mk (EndpointIdent p a) { val := x, property := hx })) =
    Quot.mk (EndpointIdent p a) { val := x, property := hx }
[PROOFSTEP]
revert x
[GOAL]
case mk.inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      (fun x => Quot.mk (EndpointIdent p a) (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p)) (↑(equivIco p a) x)))
          ((fun x =>
              Quot.liftOn x (fun x => ↑↑x)
                (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (fun x => ↑↑x) a_1 = (fun x => ↑↑x) b))
            (Quot.mk (EndpointIdent p a) { val := x, property := hx })) =
        Quot.mk (EndpointIdent p a) { val := x, property := hx }
[PROOFSTEP]
dsimp only
[GOAL]
case mk.inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      Quot.mk (EndpointIdent p a)
          (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
            (↑(equivIco p a)
              (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := x, property := hx }) (fun x => ↑↑x)
                (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b)))) =
        Quot.mk (EndpointIdent p a) { val := x, property := hx }
[PROOFSTEP]
intro x hx h
[GOAL]
case mk.inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ Quot.mk (EndpointIdent p a)
      (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
        (↑(equivIco p a)
          (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := x, property := hx }) (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b)))) =
    Quot.mk (EndpointIdent p a) { val := x, property := hx }
[PROOFSTEP]
congr
[GOAL]
case mk.inl.e_a
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
      (↑(equivIco p a)
        (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := x, property := hx }) (fun x => ↑↑x)
          (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b))) =
    { val := x, property := hx }
[PROOFSTEP]
ext1
[GOAL]
case mk.inl.e_a.a
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ ↑(Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
        (↑(equivIco p a)
          (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := x, property := hx }) (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b)))) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
apply congr_arg Subtype.val ((equivIco p a).right_inv ⟨x, hx.1, hx.2.lt_of_ne h⟩)
[GOAL]
case mk.inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x => Quot.mk (EndpointIdent p a) (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p)) (↑(equivIco p a) x)))
      ((fun x =>
          Quot.liftOn x (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (fun x => ↑↑x) a_1 = (fun x => ↑↑x) b))
        (Quot.mk (EndpointIdent p a) { val := a + p, property := hx })) =
    Quot.mk (EndpointIdent p a) { val := a + p, property := hx }
[PROOFSTEP]
rw [← Quot.sound EndpointIdent.mk]
[GOAL]
case mk.inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x => Quot.mk (EndpointIdent p a) (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p)) (↑(equivIco p a) x)))
      ((fun x =>
          Quot.liftOn x (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (fun x => ↑↑x) a_1 = (fun x => ↑↑x) b))
        (Quot.mk (EndpointIdent p a) { val := a, property := (_ : a ∈ Icc a (a + p)) })) =
    Quot.mk (EndpointIdent p a) { val := a, property := (_ : a ∈ Icc a (a + p)) }
[PROOFSTEP]
dsimp only
[GOAL]
case mk.inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ Quot.mk (EndpointIdent p a)
      (Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
        (↑(equivIco p a)
          (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := a, property := (_ : a ∈ Icc a (a + p)) }) (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b)))) =
    Quot.mk (EndpointIdent p a) { val := a, property := (_ : a ∈ Icc a (a + p)) }
[PROOFSTEP]
congr
[GOAL]
case mk.inr.e_a
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
      (↑(equivIco p a)
        (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := a, property := (_ : a ∈ Icc a (a + p)) }) (fun x => ↑↑x)
          (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b))) =
    { val := a, property := (_ : a ∈ Icc a (a + p)) }
[PROOFSTEP]
ext1
[GOAL]
case mk.inr.e_a.a
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ ↑(Set.inclusion (_ : Ico a (a + p) ⊆ Icc a (a + p))
        (↑(equivIco p a)
          (Quot.liftOn (Quot.mk (EndpointIdent p a) { val := a, property := (_ : a ∈ Icc a (a + p)) }) (fun x => ↑↑x)
            (_ : ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b)))) =
    ↑{ val := a, property := (_ : a ∈ Icc a (a + p)) }
[PROOFSTEP]
apply congr_arg Subtype.val ((equivIco p a).right_inv ⟨a, le_refl a, lt_add_of_pos_right a hp.out⟩)
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ↑(equivIccQuot p a) ∘ Quotient.mk'' = fun x =>
    Quot.mk (EndpointIdent p a)
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }
[PROOFSTEP]
rw [equivIccQuot_comp_mk_eq_toIcoMod]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) }) =
    fun x =>
    Quot.mk (EndpointIdent p a)
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }
[PROOFSTEP]
funext x
[GOAL]
case h
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ Quot.mk (EndpointIdent p a)
      { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) } =
    Quot.mk (EndpointIdent p a)
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }
[PROOFSTEP]
by_cases a ≡ x [PMOD p]
[GOAL]
case h
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ Quot.mk (EndpointIdent p a)
      { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) } =
    Quot.mk (EndpointIdent p a)
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }
[PROOFSTEP]
by_cases a ≡ x [PMOD p]
[GOAL]
case pos
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a)
      { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) } =
    Quot.mk (EndpointIdent p a)
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }
[PROOFSTEP]
simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
[GOAL]
case pos
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) { val := a, property := (_ : (fun x => x ∈ Icc a (a + p)) a) } =
    Quot.mk (EndpointIdent p a) { val := a + p, property := (_ : (fun x => x ∈ Icc a (a + p)) (a + p)) }
[PROOFSTEP]
exact Quot.sound EndpointIdent.mk
[GOAL]
case neg
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a)
      { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) } =
    Quot.mk (EndpointIdent p a)
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }
[PROOFSTEP]
simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ Continuous (equivIccQuot p a).toFun
[PROOFSTEP]
rw [quotientMap_quotient_mk'.continuous_iff]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ Continuous ((equivIccQuot p a).toFun ∘ Quotient.mk')
[PROOFSTEP]
simp_rw [continuous_iff_continuousAt, continuousAt_iff_continuous_left_right]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜),
    ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x ∧
      ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
constructor
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
on_goal 1 => erw [equivIccQuot_comp_mk_eq_toIocMod]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
on_goal 1 => erw [equivIccQuot_comp_mk_eq_toIocMod]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x
[PROOFSTEP]
erw [equivIccQuot_comp_mk_eq_toIocMod]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Iic x) x
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
on_goal 2 => erw [equivIccQuot_comp_mk_eq_toIcoMod]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Iic x) x
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
on_goal 2 => erw [equivIccQuot_comp_mk_eq_toIcoMod]
[GOAL]
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
[PROOFSTEP]
erw [equivIccQuot_comp_mk_eq_toIcoMod]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Iic x) x
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Ici x) x
[PROOFSTEP]
all_goals
  apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
  rw [inducing_subtype_val.continuousWithinAt_iff]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Iic x) x
[PROOFSTEP]
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x => { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) }) (Iic x) x
[PROOFSTEP]
rw [inducing_subtype_val.continuousWithinAt_iff]
[GOAL]
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x =>
      Quot.mk (EndpointIdent p a)
        { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Ici x) x
[PROOFSTEP]
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
[GOAL]
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (fun x => { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) }) (Ici x) x
[PROOFSTEP]
rw [inducing_subtype_val.continuousWithinAt_iff]
[GOAL]
case left
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (Subtype.val ∘ fun x =>
      { val := toIocMod (_ : 0 < p) a x, property := (_ : toIocMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Iic x) x
[PROOFSTEP]
apply continuous_left_toIocMod
[GOAL]
case right
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ContinuousWithinAt
    (Subtype.val ∘ fun x =>
      { val := toIcoMod (_ : 0 < p) a x, property := (_ : toIcoMod (_ : 0 < p) a x ∈ Icc a (a + p)) })
    (Ici x) x
[PROOFSTEP]
apply continuous_right_toIcoMod
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b
[PROOFSTEP]
rintro _ _ ⟨_⟩
[GOAL]
case mk
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ restrict (Icc a (a + p)) f { val := a, property := (_ : a ∈ Icc a (a + p)) } =
    restrict (Icc a (a + p)) f { val := a + p, property := (_ : a + p ∈ Icc a (a + p)) }
[PROOFSTEP]
exact h
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (liftIco p a f)
[PROOFSTEP]
rw [liftIco_eq_lift_Icc hf]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous
    (Quot.lift (restrict (Icc a (a + p)) f)
        (_ :
          ∀ (a_1 b : ↑(Icc a (a + p))),
            EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b) ∘
      ↑(equivIccQuot p a))
[PROOFSTEP]
refine' Continuous.comp _ (homeoIccQuot p a).continuous_toFun
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous
    (Quot.lift (restrict (Icc a (a + p)) f)
      (_ :
        ∀ (a_1 b : ↑(Icc a (a + p))),
          EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b))
[PROOFSTEP]
exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)
[PROOFSTEP]
rwa [zero_add]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ f 0 = f (0 + p)
[PROOFSTEP]
rwa [zero_add]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 (0 + p))
[PROOFSTEP]
rwa [zero_add]
