awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))
simp_rw :
  (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ Prod.map mk mk ⁻¹' s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)
⊢ ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)

Tactic:
simp_rw [ContinuousOn, (surjective_mk.prodMap surjective_mk).forall, Prod.forall, Prod.map,
    continuousWithinAt_lift₂]

Premises used: Function.Surjective.forall, Function.Surjective.prodMap, Prod.map, SeparationQuotient.surjective_mk, Prod.forall, ContinuousOn, SeparationQuotient.continuousWithinAt_lift₂
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))
⊢ (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ Prod.map mk mk ⁻¹' s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)

Tactic:
rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
⊢ Continuous[_, inst_2] (uncurry (lift₂ f hf)) ↔ Continuous[instTopologicalSpaceProd, inst_2] (uncurry f)

Tactic:
simp only [← continuousOn_univ, continuousOn_lift₂, preimage_univ]

Premises used: Set.preimage_univ, SeparationQuotient.continuousOn_lift₂, continuousOn_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
simp_rw : Continuous[inst, _] (SeparationQuotient.mk ∘ f) ↔ Continuous[inst, _] (SeparationQuotient.mk ∘ g)
⊢ Continuous[inst, inst_1] f ↔ Continuous[inst, inst_1] g

Tactic:
simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]

Premises used: SeparationQuotient.isInducing_mk, Topology.IsInducing.continuous_iff
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous[inst, _] (SeparationQuotient.mk ∘ f) ↔ Continuous[inst, _] (SeparationQuotient.mk ∘ g)

Tactic:
continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, continuous_congr
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous[inst, _] (SeparationQuotient.mk ∘ f) ↔ Continuous[inst, _] (SeparationQuotient.mk ∘ g)

Tactic:
exact continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, continuous_congr
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, x_1 ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
⊢ toIcoDiv hp a =ᶠ[𝓝[≥] x] fun (x_1 : 𝕜) ↦ toIcoDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]

Premises used: Set.sub_mem_Ico_iff_left, Filter.EventuallyEq, toIcoDiv_eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
H : x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, x_1 ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)

Tactic:
apply Ico_mem_nhdsGE_of_mem

Premises used: Ico_mem_nhdsGE_of_mem
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
H : x - toIcoDiv hp a x • p ∈ Ico a (a + p)
H₁ : toIcoDiv hp a x = toIcoDiv hp a x
H₂ : 0 < p
H₃ : toIcoDiv hp a x = toIcoDiv hp a x
H₄ : 0 < p
⊢ x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)

Tactic:
rw [← sub_mem_Ico_iff_left, ← toIcoDiv_eq_iff]

Premises used: Set.sub_mem_Ico_iff_left, toIcoDiv_eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIcoDiv hp a) (Ici x) x

Tactic:
Filter.tendsto_pure.mpr (eventuallyEq_toIcoDiv_nhdsGE hp a x) |>.mono_right <| pure_le_nhds _

Premises used: Iff.mpr, ContinuousWithinAt, pure_le_nhds, Filter.tendsto_pure, eventuallyEq_toIcoDiv_nhdsGE, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, x_1 ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
⊢ toIocDiv hp a =ᶠ[𝓝[≤] x] fun (x_1 : 𝕜) ↦ toIocDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIocDiv_eq_iff, sub_mem_Ioc_iff_left]

Premises used: Set.sub_mem_Ioc_iff_left, Filter.EventuallyEq, toIocDiv_eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
H : x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, x_1 ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
apply Ioc_mem_nhdsLE_of_mem

Premises used: Ioc_mem_nhdsLE_of_mem
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
H : x - toIocDiv hp a x • p ∈ Ioc a (a + p)
H₁ : toIocDiv hp a x = toIocDiv hp a x
H₂ : 0 < p
H₃ : toIocDiv hp a x = toIocDiv hp a x
H₄ : 0 < p
⊢ x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
rw [← sub_mem_Ioc_iff_left, ← toIocDiv_eq_iff]

Premises used: Set.sub_mem_Ioc_iff_left, toIocDiv_eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIocDiv hp a) (Iic x) x

Tactic:
Filter.tendsto_pure.mpr (eventuallyEq_toIocDiv_nhdsLE hp a x) |>.mono_right <| pure_le_nhds _

Premises used: Iff.mpr, ContinuousWithinAt, pure_le_nhds, Filter.tendsto_pure, eventuallyEq_toIocDiv_nhdsLE, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIcoMod hp a) (Ici x) x

Tactic:
continuousWithinAt_id.sub <|
    (continuousWithinAt_toIcoDiv_Ici hp a x).smul continuousWithinAt_const

Premises used: ContinuousWithinAt.sub, continuousWithinAt_id, continuousWithinAt_const, continuousWithinAt_toIcoDiv_Ici, ContinuousWithinAt.smul, toIcoMod
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIocMod hp a) (Iic x) x

Tactic:
continuousWithinAt_id.sub <|
    (continuousWithinAt_toIocDiv_Iic hp a x).smul continuousWithinAt_const

Premises used: ContinuousWithinAt.sub, continuousWithinAt_id, continuousWithinAt_toIocDiv_Iic, toIocMod, continuousWithinAt_const, ContinuousWithinAt.smul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, x_1 ∈ Ico (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
⊢ toIcoDiv hp a =ᶠ[𝓝[<] x] fun (x_1 : 𝕜) ↦ toIocDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]

Premises used: Set.sub_mem_Ico_iff_left, Filter.EventuallyEq, toIcoDiv_eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
H : x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, x_1 ∈ Ico (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
apply Ico_mem_nhdsLT_of_mem

Premises used: Ico_mem_nhdsLT_of_mem
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, x_1 ∈ Ioc (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
⊢ toIocDiv hp a =ᶠ[𝓝[>] x] fun (x_1 : 𝕜) ↦ toIcoDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIocDiv_eq_iff, sub_mem_Ioc_iff_left]

Premises used: Set.sub_mem_Ioc_iff_left, Filter.EventuallyEq, toIocDiv_eq_iff
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
H : x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, x_1 ∈ Ioc (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)

Tactic:
apply Ioc_mem_nhdsGT_of_mem

Premises used: Ioc_mem_nhdsGT_of_mem
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
rw :
  (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x
⊢ toIcoDiv hp a =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ toIcoDiv hp a x

Tactic:
rw [← nhdsLT_sup_nhdsGE, Filter.EventuallyEq, Filter.eventually_sup]

Premises used: Filter.EventuallyEq, nhdsLT_sup_nhdsGE, Filter.eventually_sup
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x

Tactic:
⟨?_, eventuallyEq_toIcoDiv_nhdsGE hp a x⟩

Premises used: eventuallyEq_toIcoDiv_nhdsGE, And.intro
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine : ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x

Tactic:
refine ⟨?_, eventuallyEq_toIcoDiv_nhdsGE hp a x⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIocDiv hp a x

Tactic:
(eventuallyEq_toIcoDiv_nhdsLT hp a x).eventually

Premises used: Filter.EventuallyEq.eventually, eventuallyEq_toIcoDiv_nhdsLT
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
h : ∀ (x_1 : 𝕜), toIcoDiv hp a x = toIocDiv hp a x
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x

Tactic:
convert! (eventuallyEq_toIcoDiv_nhdsLT hp a x).eventually using 3

Premises used: Filter.EventuallyEq.eventually, eventuallyEq_toIcoDiv_nhdsLT
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
x_1 : 𝕜
h : ¬a ≡ x [PMOD p]
h₁ h₂ h₃ h₄ : ¬x ≡ a [PMOD p]
⊢ toIcoDiv hp a x = toIocDiv hp a x

Tactic:
rwa [← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]

Premises used: AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ContinuousAt (toIcoDiv hp a) x

Tactic:
tendsto_nhds_of_eventually_eq <| eventuallyEq_toIcoDiv_nhds hp a hx

Premises used: ContinuousAt, eventuallyEq_toIcoDiv_nhds, tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a : 𝕜
⊢ ContinuousOn (toIcoDiv hp a) {x : 𝕜 | ¬x ≡ a [PMOD p]}

Tactic:
fun _x hx ↦
  (continuousAt_toIcoDiv hp a hx).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, continuousAt_toIcoDiv, ContinuousOn
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
rw :
  (∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x
⊢ toIocDiv hp a =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ toIocDiv hp a x

Tactic:
rw [← nhdsLE_sup_nhdsGT, Filter.EventuallyEq, Filter.eventually_sup]

Premises used: Filter.EventuallyEq, nhdsLE_sup_nhdsGT, Filter.eventually_sup
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x

Tactic:
⟨eventuallyEq_toIocDiv_nhdsLE hp a x, ?_⟩

Premises used: And.intro, eventuallyEq_toIocDiv_nhdsLE
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine : ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x

Tactic:
refine ⟨eventuallyEq_toIocDiv_nhdsLE hp a x, ?_⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIcoDiv hp a x

Tactic:
(eventuallyEq_toIocDiv_nhdsGT hp a x).eventually

Premises used: eventuallyEq_toIocDiv_nhdsGT, Filter.EventuallyEq.eventually
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
h : ∀ (x_1 : 𝕜), toIocDiv hp a x = toIcoDiv hp a x
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x

Tactic:
convert! (eventuallyEq_toIocDiv_nhdsGT hp a x).eventually using 3

Premises used: eventuallyEq_toIocDiv_nhdsGT, Filter.EventuallyEq.eventually
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
x_1 : 𝕜
h : toIcoDiv hp a x = toIocDiv hp a x
h₁ : ¬a ≡ x [PMOD p]
h₂ h₃ h₄ h₅ : ¬x ≡ a [PMOD p]
⊢ toIocDiv hp a x = toIcoDiv hp a x

Tactic:
rwa [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]

Premises used: AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, AddCommGroup.modEq_comm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ContinuousAt (toIocDiv hp a) x

Tactic:
tendsto_nhds_of_eventually_eq <| eventuallyEq_toIocDiv_nhds hp a hx

Premises used: ContinuousAt, tendsto_nhds_of_eventually_eq, eventuallyEq_toIocDiv_nhds
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a : 𝕜
⊢ ContinuousOn (toIocDiv hp a) {x : 𝕜 | ¬x ≡ a [PMOD p]}

Tactic:
fun _x hx ↦
  (continuousAt_toIocDiv hp a hx).continuousWithinAt

Premises used: continuousAt_toIocDiv, ContinuousAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a

Tactic:
IsOpen.mem_nhds ?_ ?_

Premises used: Filter.Eventually, Filter.EventuallyEq, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine_1 : IsOpen[inst_4] {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x}
refine_2 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x} x
⊢ toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a

Tactic:
refine IsOpen.mem_nhds ?_ ?_

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine_1 : IsOpen[inst_4] (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))
⊢ IsOpen[inst_4] {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]

Premises used: Ico_eq_locus_Ioc_eq_iUnion_Ioo
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst_4] (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))

Tactic:
isOpen_iUnion fun i => isOpen_Ioo

Premises used: isOpen_Ioo, isOpen_iUnion
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst_4] (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))

Tactic:
exact isOpen_iUnion fun i => isOpen_Ioo

Premises used: isOpen_Ioo, isOpen_iUnion
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine_2 : toIcoMod hp a x = toIocMod hp a x
refine_2₁ : ¬a ≡ x [PMOD p]
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : ¬x ≡ a [PMOD p]
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x} x

Tactic:
rwa [mem_setOf_eq, ← not_modEq_iff_toIcoMod_eq_toIocMod hp, AddCommGroup.modEq_comm]

Premises used: AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod, Set.mem_setOf_eq, AddCommGroup.modEq_comm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ContinuousAt (toIcoMod hp a) x

Tactic:
continuousAt_id.sub <| tendsto_nhds_of_eventually_eq <|
    (eventuallyEq_toIcoDiv_nhds hp a hx).fun_comp (· • p)

Premises used: eventuallyEq_toIcoDiv_nhds, ContinuousAt.sub, tendsto_nhds_of_eventually_eq, HSMul.hSMul, Filter.EventuallyEq.fun_comp, toIcoMod, continuousAt_id
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ContinuousAt (toIocMod hp a) x

Tactic:
continuousAt_id.sub <| tendsto_nhds_of_eventually_eq <|
    (eventuallyEq_toIocDiv_nhds hp a hx).fun_comp (· • p)

Premises used: ContinuousAt.sub, tendsto_nhds_of_eventually_eq, toIocMod, eventuallyEq_toIocDiv_nhds, HSMul.hSMul, Filter.EventuallyEq.fun_comp, continuousAt_id
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
x : 𝕜
⊢ (↑(n • x) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
rfl

Premises used: QuotientAddGroup.Quotient.addGroup._aux_4, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
x : 𝕜
⊢ (↑(n • x) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) n (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
rfl

Premises used: QuotientAddGroup.Quotient.addGroup._aux_9, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x y : 𝕜
⊢ (↑(x + y) : 𝕜 ⧸ zmultiples p) =
    HAdd.hAdd (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑y : 𝕜 ⧸ zmultiples p)

Tactic:
rfl

Premises used: Quotient.map₂, rfl