feat(Topology/Instances/AddCircle): add Ioc analogues of lift and equiv lemmas (#37570)

Add AddCircle lemmas:
- `liftIoc_eq_liftIco_of_ne`: the Ioc and Ico lifts agree away from the basepoint
- `coe_eq_coe_iff_of_mem_Ioc`: Ioc analogue of `coe_eq_coe_iff_of_mem_Ico`
- `eq_coe_Ioc`: Ioc analogue of `eq_coe_Ico`
- `coe_equivIoc`: Ioc analogue of `coe_equivIco`
- `equivIoc_coe_of_mem`: if `y ∈ Ioc a (a + p)`, then `equivIoc p a y = y`

Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project.

Co-authored-by: James Sundstrom <James.Sundstrom@gmail.com>
Co-authored-by: Leo Diedering <129694072+ldiedering@users.noreply.github.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 4 people

Mathlib/Topology/Instances/AddCircle/Defs.lean

@@ -328,6 +328,26 @@ theorem equivIco_coe_eq {x : 𝕜} (hx : x ∈ Ico a (a + p)) : (equivIco p a) x
 theorem equivIoc_coe_eq {x : 𝕜} (hx : x ∈ Ioc a (a + p)) : (equivIoc p a) x = ⟨x, hx⟩ := by
   rw [Equiv.apply_eq_iff_eq_symm_apply, equivIoc, QuotientAddGroup.equivIocMod_symm_apply]
 
+@[simp]
+lemma coe_equivIco {y : AddCircle p} :
+    (equivIco p a y : AddCircle p) = y :=
+  (equivIco p a).left_inv y
+
+@[simp]
+lemma coe_equivIoc {y : AddCircle p} :
+    (equivIoc p a y : AddCircle p) = y :=
+  (equivIoc p a).left_inv y
+
+lemma equivIco_coe_of_mem {y : 𝕜} (hy : y ∈ Ico a (a + p)) :
+    equivIco p a y = y := by
+  have : equivIco p a y = ⟨y, hy⟩ := (equivIco p a).right_inv ⟨y, hy⟩
+  simp [this]
+
+lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Ioc a (a + p)) :
+    equivIoc p a y = y := by
+  have : equivIoc p a y = ⟨y, hy⟩ := (equivIoc p a).right_inv ⟨y, hy⟩
+  simp [this]
+
 theorem coe_eq_coe_iff_of_mem_Ico {x y : 𝕜} (hx : x ∈ Ico a (a + p)) (hy : y ∈ Ico a (a + p)) :
     (x : AddCircle p) = y ↔ x = y := by
   refine ⟨fun h => ?_, by tauto⟩
@@ -336,6 +356,15 @@ theorem coe_eq_coe_iff_of_mem_Ico {x y : 𝕜} (hx : x ∈ Ico a (a + p)) (hy :
   rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
   exact h
 
+/-- Ioc version of `coe_eq_coe_iff_of_mem_Ico`. -/
+lemma coe_eq_coe_iff_of_mem_Ioc {x y : 𝕜} (hx : x ∈ Ioc a (a + p)) (hy : y ∈ Ioc a (a + p)) :
+    (x : AddCircle p) = y ↔ x = y := by
+  refine ⟨fun h => ?_, by tauto⟩
+  suffices (⟨x, hx⟩ : Ioc a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
+  apply_fun equivIoc p a at h
+  rw [← (equivIoc p a).right_inv ⟨x, hx⟩, ← (equivIoc p a).right_inv ⟨y, hy⟩]
+  exact h
+
 theorem liftIco_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ico a (a + p)) :
     liftIco p a f ↑x = f x := by
   simp [liftIco, equivIco_coe_eq hx]
@@ -344,17 +373,29 @@ theorem liftIoc_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ioc a (a + p))
     liftIoc p a f ↑x = f x := by
   simp [liftIoc, equivIoc_coe_eq hx]
 
+theorem liftIoc_eq_liftIco_of_ne {f : 𝕜 → B} {x : AddCircle p}
+    (x_ne_a : x ≠ a) : liftIoc p a f x = liftIco p a f x := by
+  have x_eq_b : x = ↑(equivIco p a x) := coe_equivIco.symm
+  rw [x_eq_b, liftIco_coe_apply (equivIco p a x).coe_prop]
+  exact liftIoc_coe_apply (by grind)
+
 lemma liftIco_comp_apply {α β : Type*} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} :
     liftIco p a (g ∘ f) x = g (liftIco p a f x) := rfl
 
 lemma liftIoc_comp_apply {α β : Type*} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} :
     liftIoc p a (g ∘ f) x = g (liftIoc p a f x) := rfl
 
-lemma eq_coe_Ico (a : AddCircle p) : ∃ b, b ∈ Ico 0 p ∧ ↑b = a := by
+lemma eq_coe_Ico (a : AddCircle p) : ∃ b ∈ Ico 0 p, ↑b = a := by
   let b := QuotientAddGroup.equivIcoMod hp.out 0 a
   exact ⟨b.1, by simpa only [zero_add] using b.2,
     (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩
 
+/-- `Ioc` version of `eq_coe_Ico`. -/
+lemma eq_coe_Ioc (a : AddCircle p) : ∃ b ∈ Ioc 0 p, ↑b = a := by
+  let b := QuotientAddGroup.equivIocMod hp.out 0 a
+  exact ⟨b.1, by simpa only [zero_add] using b.2,
+    (QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩
+
 lemma coe_eq_zero_iff_of_mem_Ico (ha : a ∈ Ico 0 p) :
     (a : AddCircle p) = 0 ↔ a = 0 := by
   have h0 : 0 ∈ Ico 0 (0 + p) := by simpa [zero_add, left_mem_Ico] using hp.out