awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
inl :
  Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
      ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
        (Quot.liftOn (r := EndpointIdent p a)
          (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
          (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯)) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a)
      (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
        ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
          (Quot.liftOn (r := EndpointIdent p a)
            (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
            (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))

Tactic:
congr
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
inl :
  (↑(Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
          ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
            (Quot.liftOn (r := EndpointIdent p a)
              (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
              (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))) :
      𝕜) =
    (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx) : 𝕜)
⊢ Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
      ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
        (Quot.liftOn (r := EndpointIdent p a)
          (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
          (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯)) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx

Tactic:
ext1
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ (↑(Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
          ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
            (Quot.liftOn (r := EndpointIdent p a)
              (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
              (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))) :
      𝕜) =
    (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx) : 𝕜)

Tactic:
apply congr_arg Subtype.val ((equivIco p a).right_inv ⟨x, hx.1, hx.2.lt_of_ne h⟩)

Premises used: AddCircle.equivIco, Equiv.right_inv, Subtype.mk, LE.le.lt_of_ne, congr_arg, And.right, And.left, And.intro, Subtype.val
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
inr :
  Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    ((fun (x : 𝕋) ↦
        (Quot.mk (EndpointIdent p a)
            (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
              ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
          Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
      ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
          x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
            ⋯)
        (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    ((fun (x : 𝕋) ↦
        (Quot.mk (EndpointIdent p a)
            (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
              ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
          Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
      ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
          x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
            ⋯)
        (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) hx))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) hx))

Tactic:
rw [← Quot.sound EndpointIdent.mk]

Premises used: Quot.sound, AddCircle.EndpointIdent.mk
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
inr :
  Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a)
      (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
        ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
          (Quot.liftOn (r := EndpointIdent p a)
            (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
            (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    ((fun (x : 𝕋) ↦
        (Quot.mk (EndpointIdent p a)
            (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
              ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
          Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
      ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
          x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
            ⋯)
        (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))

Tactic:
dsimp only
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
inr :
  Eq (α := (↑(Icc a (a + p)) : Type u_1))
    (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
        ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
          (Quot.liftOn (r := EndpointIdent p a)
            (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
            (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯)) :
      (↑(Icc a (a + p)) : Type u_1))
    (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯ : { x : 𝕜 // x ∈ Icc a (a + p) })
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a)
      (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
        ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
          (Quot.liftOn (r := EndpointIdent p a)
            (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
            (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))

Tactic:
congr
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
inr :
  (↑(Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
          ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
            (Quot.liftOn (r := EndpointIdent p a)
              (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
              (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))) :
      𝕜) =
    (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯ : { x : 𝕜 // x ∈ Icc a (a + p) }) : 𝕜)
⊢ Eq (α := (↑(Icc a (a + p)) : Type u_1))
    (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
        ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
          (Quot.liftOn (r := EndpointIdent p a)
            (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
            (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯)) :
      (↑(Icc a (a + p)) : Type u_1))
    (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯ : { x : 𝕜 // x ∈ Icc a (a + p) })

Tactic:
ext1
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (↑(Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
          ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
            (Quot.liftOn (r := EndpointIdent p a)
              (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
              (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))) :
      𝕜) =
    (↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯ : { x : 𝕜 // x ∈ Icc a (a + p) }) : 𝕜)

Tactic:
apply congr_arg Subtype.val
          ((equivIco p a).right_inv ⟨a, le_refl a, lt_add_of_pos_right a hp.out⟩)

Premises used: AddCircle.equivIco, le_refl, lt_add_of_pos_right, Equiv.right_inv, Subtype.mk, congr_arg, And.intro, Subtype.val, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
⊢ Eq (α := 𝕜 → Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (comp (β := 𝕋) (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)) Quotient.mk'') fun (x : 𝕜) ↦
    Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯)

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, toIcoMod, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
rw :
  Eq.{u_1 + 1} (α := 𝕜 → Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    fun (x : 𝕜) ↦
    Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯)
⊢ Eq (α := 𝕜 → Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (comp (β := 𝕋) (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)) Quotient.mk'') fun (x : 𝕜) ↦
    Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯)

Tactic:
rw [equivIccQuot_comp_mk_eq_toIcoMod]

Premises used: AddCircle.equivIccQuot_comp_mk_eq_toIcoMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
h :
  ∀ (x : 𝕜),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
⊢ Eq.{u_1 + 1} (α := 𝕜 → Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    fun (x : 𝕜) ↦
    Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯)

Tactic:
funext x
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
pos :
  ∀ (h : a ≡ x [PMOD p]),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
neg :
  ∀ (h : ¬a ≡ x [PMOD p]),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))

Tactic:
by_cases h : a ≡ x [PMOD p]
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
pos :
  Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯))
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))

Tactic:
simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]

Premises used: AddCommGroup.modEq_iff_toIcoMod_eq_left, AddCommGroup.modEq_iff_toIocMod_eq_right, Iff.mp, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯))

Tactic:
Quot.sound EndpointIdent.mk

Premises used: Quot.sound, AddCircle.EndpointIdent.mk
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯))

Tactic:
exact Quot.sound EndpointIdent.mk

Premises used: Quot.sound, AddCircle.EndpointIdent.mk
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))

Tactic:
simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]

Premises used: AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod, Iff.mp, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
simp_rw :
  ∀ (x : 𝕜),
    ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
        (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x ∧
      ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
        (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), instTopologicalSpaceQuot]
    (Equiv.toFun (equivIccQuot p a))

Tactic:
simp_rw [isQuotientMap_quotient_mk'.continuous_iff, continuous_iff_continuousAt,
      continuousAt_iff_continuous_left_right]

Premises used: isQuotientMap_quotient_mk', continuousAt_iff_continuous_left_right, Topology.IsQuotientMap.continuous_iff, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
left :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x
right :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
left :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
    (Iic x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x

Tactic:
erw [equivIccQuot_comp_mk_eq_toIocMod]

Premises used: AddCircle.equivIccQuot_comp_mk_eq_toIocMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
left :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
    (Iic x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x

Tactic:
on_goal 1 => erw [equivIccQuot_comp_mk_eq_toIocMod]

Premises used: AddCircle.equivIccQuot_comp_mk_eq_toIocMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
right :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Ici x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x

Tactic:
erw [equivIccQuot_comp_mk_eq_toIcoMod]

Premises used: AddCircle.equivIccQuot_comp_mk_eq_toIcoMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
right :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Ici x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x

Tactic:
on_goal 2 => erw [equivIccQuot_comp_mk_eq_toIcoMod]

Premises used: AddCircle.equivIccQuot_comp_mk_eq_toIcoMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
left :
  ContinuousWithinAt (Y := (↑(Icc a (a + p)) : Type u_1))
    (fun (x : 𝕜) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯) (Iic x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
    (Iic x) x

Tactic:
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt

Premises used: Continuous.continuousAt, continuous_quot_mk, ContinuousAt.comp_continuousWithinAt
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
left :
  ContinuousWithinAt (Y := 𝕜)
    (comp (β := { x : 𝕜 // x ∈ Icc a (a + p) }) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p))) fun (x : 𝕜) ↦
      Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯)
    (Iic x) x
⊢ ContinuousWithinAt (Y := (↑(Icc a (a + p)) : Type u_1))
    (fun (x : 𝕜) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯) (Iic x) x

Tactic:
rw [IsInducing.subtypeVal.continuousWithinAt_iff]

Premises used: Topology.IsInducing.continuousWithinAt_iff, Topology.IsInducing.subtypeVal