awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
y : Y
e : y ⤳ f x
⊢ ∃ (a' : X), (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = y
have obtain : ∀ (y : X) (e : f y ⤳ f x), ∃ (a' : X), (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y
Tactic: obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩
Cleared hypotheses: y, e
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
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
g : Y → Z
hf : GeneralizingMap f
hg : GeneralizingMap g
⊢ GeneralizingMap (g ∘ f)
have simp : ∀ (hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s))
  (hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)) (s : Set X),
  StableUnderGeneralization s → StableUnderGeneralization (g '' f '' s)
Tactic: simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ preimage (β := SeparationQuotient X) mk (mk '' s) = s
have refine : preimage (β := SeparationQuotient X) mk (mk '' s) ⊆ s
Tactic: refine Subset.antisymm ?_ (subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ preimage (β := SeparationQuotient X) mk (mk '' s) = s
have refine : preimage (β := SeparationQuotient X) mk (mk '' s) ⊆ s
Tactic: refine Subset.antisymm ?_ (subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsClosed.{u_1} (X := SeparationQuotient X) (range mk)
have rw : IsClosed.{u_1} (X := SeparationQuotient X) univ
Tactic: rw [range_mk]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ Eq (α := Filter (SeparationQuotient X)) (map mk (𝓝 x)) (𝓝 (mk x))
have rw : Eq (α := Filter (SeparationQuotient X)) (map mk (comap (β := SeparationQuotient X) mk (𝓝 (mk x)))) (𝓝 (mk x))
Tactic: rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
rw : Eq (α := Filter (SeparationQuotient X)) (map mk (comap (β := SeparationQuotient X) mk (𝓝 (mk x)))) (𝓝 (mk x))
⊢ Eq (α := Filter (SeparationQuotient X)) (map mk (𝓝 x)) (𝓝 (mk x))
have rw₁ : Eq (α := Filter (SeparationQuotient X)) (𝓝 (mk x)) (𝓝 (mk x))
Tactic: rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ Eq (α := Filter (SeparationQuotient X)) (map mk (𝓝ˢ s)) (𝓝ˢ (mk '' s))
have rw : Eq (α := Filter (SeparationQuotient X)) (map mk (comap (β := SeparationQuotient X) mk (𝓝ˢ (mk '' s)))) (𝓝ˢ (mk '' s))
Tactic: rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  Eq (α := Filter (SeparationQuotient X)) (map mk (comap (β := SeparationQuotient X) mk (𝓝ˢ (mk '' s)))) (𝓝ˢ (mk '' s))
⊢ Eq (α := Filter (SeparationQuotient X)) (map mk (𝓝ˢ s)) (𝓝ˢ (mk '' s))
have rw₁ : Eq (α := Filter (SeparationQuotient X)) (𝓝ˢ (mk '' s)) (𝓝ˢ (mk '' s))
Tactic: rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
| comap mk (𝓝ˢ t)
have rw : 𝓝ˢ (mk ⁻¹' t)
Tactic: rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
have conv_lhs : comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
Tactic: conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
conv_lhs : comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
have conv_lhs₁ : 𝓝ˢ (mk ⁻¹' t) = 𝓝ˢ (mk ⁻¹' t)
Tactic: conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
⊢ Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 (x, y)))
    (𝓝 (mk x, mk y))
have rw : Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y))
  (𝓝 (mk x, mk y))
Tactic: rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw :
  Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y))
    (𝓝 (mk x, mk y))
⊢ Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 (x, y)))
    (𝓝 (mk x, mk y))
have rw₁ : SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (map mk (𝓝 x)) (map mk (𝓝 y)) =
  𝓝 (mk x, mk y)
Tactic: rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw :
  Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y))
    (𝓝 (mk x, mk y))
rw₁ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (map mk (𝓝 x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
⊢ Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 (x, y)))
    (𝓝 (mk x, mk y))
have rw₂ : SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (map mk (𝓝 y)) =
  𝓝 (mk x, mk y)
Tactic: rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw :
  Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y))
    (𝓝 (mk x, mk y))
rw₁ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (map mk (𝓝 x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
rw₂ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
⊢ Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 (x, y)))
    (𝓝 (mk x, mk y))
have rw₃ : SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y)) =
  𝓝 (mk x, mk y)
Tactic: rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw :
  Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y))
    (𝓝 (mk x, mk y))
rw₁ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (map mk (𝓝 x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
rw₂ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
rw₃ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y)) =
    𝓝 (mk x, mk y)
⊢ Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 (x, y)))
    (𝓝 (mk x, mk y))
have rw₄ : SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y)) =
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y))
Tactic: rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
have rw : map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x
Tactic: rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
rw : map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
have rw₁ : map mk (𝓝 x ⊓ comap mk (𝓟 s)) = 𝓝[s] mk x
Tactic: rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
rw : map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x
rw₁ : map mk (𝓝 x ⊓ comap mk (𝓟 s)) = 𝓝[s] mk x
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
have rw₂ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝[s] mk x
Tactic: rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
rw : map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x
rw₁ : map mk (𝓝 x ⊓ comap mk (𝓟 s)) = 𝓝[s] mk x
rw₂ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝[s] mk x
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
have rw₃ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
Tactic: rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
rw : map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x
rw₁ : map mk (𝓝 x ⊓ comap mk (𝓟 s)) = 𝓝[s] mk x
rw₂ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝[s] mk x
rw₃ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
have rw₄ : 𝓝 (mk x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
Tactic: rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
have rw : Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
Tactic: rw [← map_prod_map_mk_nhds, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
have rw : Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
  Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
Tactic: rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
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))
⊢ ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)
have 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)
Tactic: simp_rw [ContinuousOn, (surjective_mk.prodMap surjective_mk).forall, Prod.forall, Prod.map,
    continuousWithinAt_lift₂]
-- Lean 4 proof step from Mathlib.Topology.Inseparable (goal)
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, inst_1] f ↔ Continuous[inst, inst_1] g
have simp_rw : Continuous[inst, _] (SeparationQuotient.mk ∘ f) ↔ Continuous[inst, _] (SeparationQuotient.mk ∘ g)
Tactic: simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ toIcoDiv hp a =ᶠ[𝓝[≥] x] fun (x_1 : 𝕜) ↦ toIcoDiv hp a x
have simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, x_1 ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
Tactic: simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, x_1 ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
have H : x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
Tactic: apply Ico_mem_nhdsGE_of_mem
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
have H : x - toIcoDiv hp a x • p ∈ Ico a (a + p)
Tactic: rw [← sub_mem_Ico_iff_left, ← toIcoDiv_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
have H₁ : toIcoDiv hp a x = toIcoDiv hp a x
Tactic: rw [← sub_mem_Ico_iff_left, ← toIcoDiv_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ toIocDiv hp a =ᶠ[𝓝[≤] x] fun (x_1 : 𝕜) ↦ toIocDiv hp a x
have simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, x_1 ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
Tactic: simp only [Filter.EventuallyEq, toIocDiv_eq_iff, sub_mem_Ioc_iff_left]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, x_1 ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
have H : x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
Tactic: apply Ioc_mem_nhdsLE_of_mem
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
have H : x - toIocDiv hp a x • p ∈ Ioc a (a + p)
Tactic: rw [← sub_mem_Ioc_iff_left, ← toIocDiv_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
have H₁ : toIocDiv hp a x = toIocDiv hp a x
Tactic: rw [← sub_mem_Ioc_iff_left, ← toIocDiv_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ toIcoDiv hp a =ᶠ[𝓝[<] x] fun (x_1 : 𝕜) ↦ toIocDiv hp a x
have simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, x_1 ∈ Ico (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
Tactic: simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, x_1 ∈ Ico (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
have H : x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
Tactic: apply Ico_mem_nhdsLT_of_mem
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ toIocDiv hp a =ᶠ[𝓝[>] x] fun (x_1 : 𝕜) ↦ toIcoDiv hp a x
have simp : ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, x_1 ∈ Ioc (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
Tactic: simp only [Filter.EventuallyEq, toIocDiv_eq_iff, sub_mem_Ioc_iff_left]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, x_1 ∈ Ioc (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
have H : x ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • p)
Tactic: apply Ioc_mem_nhdsGT_of_mem
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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]
⊢ toIcoDiv hp a =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ toIcoDiv hp a x
have 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
Tactic: rw [← nhdsLT_sup_nhdsGE, Filter.EventuallyEq, Filter.eventually_sup]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have refine : ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x
Tactic: refine ⟨?_, eventuallyEq_toIcoDiv_nhdsGE hp a x⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have h : ∀ (x_1 : 𝕜), toIcoDiv hp a x = toIocDiv hp a x
Tactic: convert! (eventuallyEq_toIcoDiv_nhdsLT hp a x).eventually using 3
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ toIcoDiv hp a x = toIocDiv hp a x
have h : ¬a ≡ x [PMOD p]
Tactic: rwa [← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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]
⊢ toIocDiv hp a =ᶠ[𝓝 x] fun (x_1 : 𝕜) ↦ toIocDiv hp a x
have 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
Tactic: rw [← nhdsLE_sup_nhdsGT, Filter.EventuallyEq, Filter.eventually_sup]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have refine : ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x
Tactic: refine ⟨eventuallyEq_toIocDiv_nhdsLE hp a x, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have h : ∀ (x_1 : 𝕜), toIocDiv hp a x = toIcoDiv hp a x
Tactic: convert! (eventuallyEq_toIocDiv_nhdsGT hp a x).eventually using 3
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
⊢ toIocDiv hp a x = toIcoDiv hp a x
have h : toIcoDiv hp a x = toIocDiv hp a x
Tactic: rwa [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ toIocDiv hp a x = toIcoDiv hp a x
have h₁ : ¬a ≡ x [PMOD p]
Tactic: rwa [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
have refine_1 : IsOpen[inst_4] {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x}
Tactic: refine IsOpen.mem_nhds ?_ ?_