𝕜 : Type u_1
B : Type ?u.328688
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)) }
𝕜 : Type u_1
B : Type ?u.328688
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)) }
rw [equivIccQuot_comp_mk_eq_toIcoMod]
case h
𝕜 : Type u_1
B : Type ?u.328688
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)) }
𝕜 : Type u_1
B : Type ?u.328688
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)) }
funext x
case pos
𝕜 : Type u_1
B : Type ?u.328688
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)) }

case neg
𝕜 : Type u_1
B : Type ?u.328688
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)) }
case h
𝕜 : Type u_1
B : Type ?u.328688
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)) }
by_cases a ≡ x [PMOD p]
case pos
𝕜 : Type u_1
B : Type ?u.328688
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)) }
case pos
𝕜 : Type u_1
B : Type ?u.328688
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)) }
simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
no goals
case pos
𝕜 : Type u_1
B : Type ?u.328688
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)) }
exact Quot.sound EndpointIdent.mk
no goals
case neg
𝕜 : Type u_1
B : Type ?u.328688
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)) }
simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]