awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
a : AddCircle p
b : (↑(Ioc 0 (0 + p)) : Type u_1) :=
  (QuotientAddGroup.equivIocMod ⋯ 0 : (a : 𝕜 ⧸ zmultiples p) → (↑(Ioc 0 (0 + p)) : Type u_1)) a
⊢ ∃ b ∈ Ioc 0 p, (↑b : 𝕜 ⧸ zmultiples p) = a

Tactic:
exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
⊢ 0 ∈ Ico 0 (0 + p)

Tactic:
simpa [zero_add, left_mem_Ico] using hp.out

Premises used: Set.left_mem_Ico, zero_add, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
⊢ 0 ∈ Ico 0 (0 + p)

Tactic:
have h0 : 0 ∈ Ico 0 (0 + p) := by simpa [zero_add, left_mem_Ico] using hp.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
rwa rwa₁ rwa₂ rwa₃ : a ∈ Ico 0 p
⊢ a ∈ Ico 0 (0 + p)

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ a ∈ Ico 0 (0 + p)

Tactic:
have ha' : a ∈ Ico 0 (0 + p) := by rwa [zero_add]
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
rw :
  Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) (↑0 : 𝕜 ⧸ zmultiples p)
rw₁ rw₂ :
  Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔ a = 0

Tactic:
rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]

Premises used: AddCircle.coe_eq_coe_iff_of_mem_Ico, QuotientAddGroup.mk_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
⊢ Continuous[instTopologicalSpaceSubtype, QuotientAddGroup.instTopologicalSpace (zmultiples p)]
    (⇑(Equiv.symm (equivIco p a)) : (a : (↑(Ico a (a + p)) : Type u_1)) → AddCircle p)

Tactic:
continuous_quotient_mk'.comp continuous_subtype_val

Premises used: continuous_subtype_val, continuous_quotient_mk', Continuous.comp, Quotient.mk'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
⊢ Continuous[instTopologicalSpaceSubtype, QuotientAddGroup.instTopologicalSpace (zmultiples p)]
    (⇑(Equiv.symm (equivIoc p a)) : (a : (↑(Ioc a (a + p)) : Type u_1)) → AddCircle p)

Tactic:
continuous_quotient_mk'.comp continuous_subtype_val

Premises used: continuous_subtype_val, continuous_quotient_mk', Continuous.comp, Quotient.mk'
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ (↑a : 𝕜 ⧸ zmultiples p)
H :
  ∀ (z : 𝕜) (hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)),
    ContinuousAt (X := AddCircle p) (Y := (↑(Ico a (a + p)) : Type u_1))
      (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)
⊢ ContinuousAt (Y := (↑(Ico a (a + p)) : Type u_1))
    (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x

Tactic:
induction x using QuotientAddGroup.induction_on
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
H :
  LE.le (α := Filter (↑(Ico a (a + p)) : Type u_1))
    (Filter.map
        (comp (β := AddCircle p) (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1))
          QuotientAddGroup.mk)
        (𝓝 z) :
      Filter (↑(Ico a (a + p)) : Type u_1))
    (𝓝 ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
      Filter (↑(Ico a (a + p)) : Type u_1))
⊢ ContinuousAt (X := AddCircle p) (Y := (↑(Ico a (a + p)) : Type u_1))
    (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)

Tactic:
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]

Premises used: ContinuousAt, Filter.map_map, Filter.Tendsto, QuotientAddGroup.nhds_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
⊢ LE.le (α := Filter (↑(Ico a (a + p)) : Type u_1))
    (Filter.map
        (comp (β := AddCircle p) (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1))
          QuotientAddGroup.mk)
        (𝓝 z) :
      Filter (↑(Ico a (a + p)) : Type u_1))
    (𝓝 ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
      Filter (↑(Ico a (a + p)) : Type u_1))

Tactic:
(continuousAt_toIcoMod hp.out a <| not_modEq_iff_ne_mod_zmultiples.mpr hx).codRestrict _

Premises used: Iff.mpr, Quotient.liftOn', Set.Mem, ContinuousAt, Function.Periodic.lift, continuousAt_toIcoMod, ContinuousAt.codRestrict, AddCommGroup.not_modEq_iff_ne_mod_zmultiples, Filter.Tendsto, Set.codRestrict, toIcoMod, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
⊢ LE.le (α := Filter (↑(Ico a (a + p)) : Type u_1))
    (Filter.map
        (comp (β := AddCircle p) (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1))
          QuotientAddGroup.mk)
        (𝓝 z) :
      Filter (↑(Ico a (a + p)) : Type u_1))
    (𝓝 ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
      Filter (↑(Ico a (a + p)) : Type u_1))

Tactic:
exact (continuousAt_toIcoMod hp.out a <| not_modEq_iff_ne_mod_zmultiples.mpr hx).codRestrict _

Premises used: Iff.mpr, continuousAt_toIcoMod, ContinuousAt.codRestrict, AddCommGroup.not_modEq_iff_ne_mod_zmultiples, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ (↑a : 𝕜 ⧸ zmultiples p)
H :
  ∀ (z : 𝕜) (hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)),
    ContinuousAt (X := AddCircle p) (Y := (↑(Ioc a (a + p)) : Type u_1))
      (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)
⊢ ContinuousAt (Y := (↑(Ioc a (a + p)) : Type u_1))
    (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) x

Tactic:
induction x using QuotientAddGroup.induction_on
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
H :
  LE.le (α := Filter (↑(Ioc a (a + p)) : Type u_1))
    (Filter.map
        (comp (β := AddCircle p) (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1))
          QuotientAddGroup.mk)
        (𝓝 z) :
      Filter (↑(Ioc a (a + p)) : Type u_1))
    (𝓝 ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
      Filter (↑(Ioc a (a + p)) : Type u_1))
⊢ ContinuousAt (X := AddCircle p) (Y := (↑(Ioc a (a + p)) : Type u_1))
    (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)

Tactic:
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]

Premises used: ContinuousAt, Filter.map_map, Filter.Tendsto, QuotientAddGroup.nhds_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
⊢ LE.le (α := Filter (↑(Ioc a (a + p)) : Type u_1))
    (Filter.map
        (comp (β := AddCircle p) (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1))
          QuotientAddGroup.mk)
        (𝓝 z) :
      Filter (↑(Ioc a (a + p)) : Type u_1))
    (𝓝 ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
      Filter (↑(Ioc a (a + p)) : Type u_1))

Tactic:
(continuousAt_toIocMod hp.out a <| not_modEq_iff_ne_mod_zmultiples.mpr hx).codRestrict _

Premises used: Iff.mpr, continuousAt_toIocMod, Quotient.liftOn', Set.Mem, ContinuousAt, Function.Periodic.lift, ContinuousAt.codRestrict, AddCommGroup.not_modEq_iff_ne_mod_zmultiples, Filter.Tendsto, toIocMod, Set.codRestrict, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
⊢ LE.le (α := Filter (↑(Ioc a (a + p)) : Type u_1))
    (Filter.map
        (comp (β := AddCircle p) (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1))
          QuotientAddGroup.mk)
        (𝓝 z) :
      Filter (↑(Ioc a (a + p)) : Type u_1))
    (𝓝 ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
      Filter (↑(Ioc a (a + p)) : Type u_1))

Tactic:
exact (continuousAt_toIocMod hp.out a <| not_modEq_iff_ne_mod_zmultiples.mpr hx).codRestrict _

Premises used: Iff.mpr, continuousAt_toIocMod, ContinuousAt.codRestrict, AddCommGroup.not_modEq_iff_ne_mod_zmultiples, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x_1 : AddCircle p
inst_6 : DiscreteTopology.{u_1} ↥(zmultiples p)
x : 𝕜
hx : x ∈ Ioo a (a + p)
hx' : Membership.mem (γ := Set (AddCircle p)) {(↑a : 𝕜 ⧸ zmultiples p)} (↑x : 𝕜 ⧸ zmultiples p)
⊢ False

Tactic:
hx.1.ne' ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx)
      (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx')

Premises used: Iff.mpr, lt_add_of_pos_right, Set.left_mem_Ico, AddCircle.coe_eq_coe_iff_of_mem_Ico, LT.lt.ne', Set.Ioo_subset_Ico_self, And.left, Iff.mp, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x_1 : AddCircle p
inst_6 : DiscreteTopology.{u_1} ↥(zmultiples p)
x : 𝕜
hx : x ∈ Ioo a (a + p)
hx' : Membership.mem (γ := Set (AddCircle p)) {(↑a : 𝕜 ⧸ zmultiples p)} (↑x : 𝕜 ⧸ zmultiples p)
⊢ False

Tactic:
exact hx.1.ne' ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx)
      (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx')

Premises used: Iff.mpr, lt_add_of_pos_right, Set.left_mem_Ico, AddCircle.coe_eq_coe_iff_of_mem_Ico, LT.lt.ne', Set.Ioo_subset_Ico_self, And.left, Iff.mp, Fact.out
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x_1 : AddCircle p
inst_6 : DiscreteTopology.{u_1} ↥(zmultiples p)
x : AddCircle p
hx : Membership.mem (γ := Set (AddCircle p)) {(↑a : 𝕜 ⧸ zmultiples p)}ᶜ x
⊢ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜) ∈ Ioo a (a + p)

Tactic:
(eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left
      (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _)

Premises used: AddCircle.equivIco, congrArg, Equiv.symm_apply_apply, Function.comp, Or.resolve_left, Set.eq_left_or_mem_Ioo_of_mem_Ico, Eq.symm, DFunLike.coe, Eq.trans, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x_1 : AddCircle p
inst_6 : DiscreteTopology.{u_1} ↥(zmultiples p)
x : AddCircle p
hx : Membership.mem (γ := Set (AddCircle p)) {(↑a : 𝕜 ⧸ zmultiples p)}ᶜ x
⊢ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜) ∈ Ioo a (a + p)

Tactic:
exact (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left
      (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _)

Premises used: AddCircle.equivIco, congrArg, Equiv.symm_apply_apply, Function.comp, Or.resolve_left, Set.eq_left_or_mem_Ioo_of_mem_Ico, Eq.symm, DFunLike.coe, Eq.trans, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
inst_6 : DiscreteTopology.{u_1} ↥(zmultiples p)
⊢ ContinuousOn (Y := 𝕜)
    (fun (x : AddCircle p) ↦ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜))
    {(↑a : 𝕜 ⧸ zmultiples p)}ᶜ

Tactic:
continuousOn_of_forall_continuousAt
      (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a)

Premises used: continuousAt_subtype_val, continuousOn_of_forall_continuousAt, Function.comp, ContinuousAt.comp, AddCircle.continuousAt_equivIco
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
inst_6 : DiscreteTopology.{u_1} ↥(zmultiples p)
⊢ ContinuousOn (Y := 𝕜)
    (fun (x : AddCircle p) ↦ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜))
    {(↑a : 𝕜 ⧸ zmultiples p)}ᶜ

Tactic:
exact continuousOn_of_forall_continuousAt
      (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a)

Premises used: continuousAt_subtype_val, continuousOn_of_forall_continuousAt, Function.comp, ContinuousAt.comp, AddCircle.continuousAt_equivIco
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
rw :
  Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
    (range fun (x : (↑(Ico a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ
⊢ Eq (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))) (QuotientAddGroup.mk '' Ico a (a + p)) univ

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
    (range fun (x : (↑(Ico a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ

Tactic:
(equivIco p a).symm.range_eq_univ

Premises used: AddCircle.equivIco, Equiv.range_eq_univ, Equiv.symm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
    (range fun (x : (↑(Ico a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ

Tactic:
exact (equivIco p a).symm.range_eq_univ

Premises used: AddCircle.equivIco, Equiv.range_eq_univ, Equiv.symm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
rw :
  Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
    (range fun (x : (↑(Ioc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ
⊢ Eq (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))) (QuotientAddGroup.mk '' Ioc a (a + p)) univ

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
    (range fun (x : (↑(Ioc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ

Tactic:
(equivIoc p a).symm.range_eq_univ

Premises used: AddCircle.equivIoc, Equiv.range_eq_univ, Equiv.symm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
    (range fun (x : (↑(Ioc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ

Tactic:
exact (equivIoc p a).symm.range_eq_univ

Premises used: AddCircle.equivIoc, Equiv.range_eq_univ, Equiv.symm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))) (QuotientAddGroup.mk '' Icc a (a + p)) univ

Tactic:
eq_top_mono (image_mono Ico_subset_Icc_self) <| coe_image_Ico_eq _ _

Premises used: Set.Ico_subset_Icc_self, Set.image_mono, eq_top_mono, AddCircle.coe_image_Ico_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
rw : EqOn f g (QuotientAddGroup.mk '' Ico a (a + p))
⊢ f = g

Tactic:
rw [← Set.eqOn_univ, ← coe_image_Ico_eq p a]

Premises used: Set.eqOn_univ, AddCircle.coe_image_Ico_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
h x hx
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
exact h x hx
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
rw : EqOn f g (QuotientAddGroup.mk '' Ioc a (a + p))
⊢ f = g

Tactic:
rw [← Set.eqOn_univ, ← coe_image_Ioc_eq p a]

Premises used: Set.eqOn_univ, AddCircle.coe_image_Ioc_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
h x hx
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
exact h x hx
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
x : 𝕜
⊢ Eq (α := AddCircle q)
    ((equivAddCircle p q hp hq : (a : AddCircle p) → AddCircle q) (↑x : 𝕜 ⧸ zmultiples p) : AddCircle q)
    ((↑(x * (p⁻¹ * q)) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples q)) :
      HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MulOpposite.unop, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
x : 𝕜
⊢ Eq (α := AddCircle p)
    (((equivAddCircle p q hp hq).symm : (a : AddCircle q) → AddCircle p) (↑x : 𝕜 ⧸ zmultiples q) : AddCircle p)
    ((↑(x * (q⁻¹ * p)) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) :
      HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MulOpposite.unop, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
hp : p ≠ 0
hq : q ≠ 0
x : 𝕜
⊢ Eq (α := AddCircle q)
    ((homeomorphAddCircle p q hp hq : (a : AddCircle p) → AddCircle q) (↑x : 𝕜 ⧸ zmultiples p) : AddCircle q)
    ((↑(x * (p⁻¹ * q)) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples q)) :
      HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MulOpposite.unop, rfl