awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto.{u_1, u_1} (α := α) fract (𝓝[≥] (↑n : α)) (𝓝[≥] 0)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ (tendsto_fract_right' _)
    (Eventually.of_forall fract_nonneg)

Premises used: tendsto_fract_right', Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Int.fract_nonneg
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
change : Continuous[instTopologicalSpaceProd, inst_7] (uncurry f ∘ Prod.map id fract)
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (st : β × α) ↦ f st.1 (fract st.2)

Tactic:
change Continuous (uncurry f ∘ Prod.map id fract)

Premises used: Continuous, Int.fract, Function.comp, id, Prod.map, Function.uncurry
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
rw : ∀ (x : β × α), ContinuousAt (uncurry f ∘ Prod.map id fract) x
⊢ Continuous[instTopologicalSpaceProd, inst_7] (uncurry f ∘ Prod.map id fract)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
inl : ∀ (n : ℤ), ContinuousAt (uncurry f ∘ Prod.map id fract) (s, (↑n : α))
inr : ∀ (ht : ¬∃ (n : ℤ), t = (↑n : α)), ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)

Tactic:
rcases em (∃ n : ℤ, t = n) with (⟨n, rfl⟩ | ht)

Premises used: Int.cast, Exists, em, Eq, rfl
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
inl :
  Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
      (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α)))) ∧
    Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
      (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, (↑n : α))

Tactic:
rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]

Premises used: Int.cast, ContinuousAt, nhdsLT_sup_nhdsGE, Filter.tendsto_sup, nhds_prod_eq, Filter.prod_sup
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
inl :
  Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
inl₁ :
  Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
      (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α)))) ∧
    Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
      (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))

Tactic:
(((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prodMap (tendsto_fract_left _))).mono_right (le_of_eq ?_)

Premises used: trivial, le_rfl, Filter.tendsto_id, Prod.mk, zero_le_one, tendsto_fract_left, And.intro, Filter.Tendsto.mono_left, Filter.Tendsto.mono_right, Filter.Tendsto.comp, le_of_eq, OfNat.ofNat, ContinuousWithinAt.tendsto, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
inl : SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] 1) ≤ 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 1)
inl₁ : 𝓝 (uncurry f (s, 1)) = 𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α)))
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))

Tactic:
refine (((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prodMap (tendsto_fract_left _))).mono_right (le_of_eq ?_)

Premises used: trivial, le_rfl, Filter.tendsto_id, Prod.mk, zero_le_one, tendsto_fract_left, And.intro, Filter.Tendsto.mono_left, Filter.Tendsto.mono_right, Filter.Tendsto.comp, le_of_eq, OfNat.ofNat, ContinuousWithinAt.tendsto, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
inl : SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Ico 0 1] 1) ≤ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Icc 0 1] 1)
⊢ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] 1) ≤ 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 1)

Tactic:
rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]

Premises used: nhdsWithin_univ, nhdsWithin_prod_eq, nhdsWithin_Ico_eq_nhdsLT, one_pos
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Ico 0 1] 1) ≤ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Icc 0 1] 1)

Tactic:
Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)

Premises used: le_rfl, Set.Ico_subset_Icc_self, Set.Mem, Filter.prod_mono, nhdsWithin_mono
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Ico 0 1] 1) ≤ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Icc 0 1] 1)

Tactic:
exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)

Premises used: le_rfl, Set.Ico_subset_Icc_self, Filter.prod_mono, nhdsWithin_mono
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 (uncurry f (s, 1)) = 𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α)))

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))

Tactic:
(((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prodMap (tendsto_fract_right _))).mono_right (le_of_eq ?_)

Premises used: trivial, le_rfl, Filter.tendsto_id, Prod.mk, zero_le_one, And.intro, Filter.Tendsto.mono_left, Filter.Tendsto.mono_right, Filter.Tendsto.comp, le_of_eq, OfNat.ofNat, ContinuousWithinAt.tendsto, tendsto_fract_right, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
inl : SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] 0) = 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 0)
inl₁ : 𝓝 (uncurry f (s, 0)) = 𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α)))
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))

Tactic:
refine (((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prodMap (tendsto_fract_right _))).mono_right (le_of_eq ?_)

Premises used: trivial, le_rfl, Filter.tendsto_id, Prod.mk, zero_le_one, And.intro, Filter.Tendsto.mono_left, Filter.Tendsto.mono_right, Filter.Tendsto.comp, le_of_eq, OfNat.ofNat, ContinuousWithinAt.tendsto, tendsto_fract_right, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] 0) = 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 0)

Tactic:
simp [nhdsWithin_prod_eq, nhdsWithin_univ]

Premises used: nhdsWithin_univ, nhdsWithin_prod_eq
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 (uncurry f (s, 0)) = 𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α)))

Tactic:
simp [nhdsWithin_prod_eq, nhdsWithin_univ]

Premises used: nhdsWithin_univ, nhdsWithin_prod_eq
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : ¬∃ (n : ℤ), t = (↑n : α)
⊢ t ≠ (↑⌊t⌋ : α)

Tactic:
replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : t ≠ (↑⌊t⌋ : α)
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)

Tactic:
(h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))

Premises used: ContinuousAt.prodMap, continuousAt_fract, ContinuousAt.comp, ContinuousOn.continuousAt, continuousAt_id
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : t ≠ (↑⌊t⌋ : α)
inr : SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1) ∈ 𝓝 (Prod.map id fract (s, t))
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)

Tactic:
refine (h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))

Premises used: ContinuousAt.prodMap, continuousAt_fract, ContinuousAt.comp, ContinuousOn.continuousAt, continuousAt_id
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : t ≠ (↑⌊t⌋ : α)
⊢ SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1) ∈ 𝓝 (Prod.map id fract (s, t))

Tactic:
prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))

Premises used: Iff.mpr, prod_mem_nhds, Set.Mem, Int.fract_pos, Prod.map, Int.fract_lt_one, Filter.univ_mem, Icc_mem_nhds
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : t ≠ (↑⌊t⌋ : α)
⊢ SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1) ∈ 𝓝 (Prod.map id fract (s, t))

Tactic:
exact prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))

Premises used: Iff.mpr, prod_mem_nhds, Int.fract_pos, Int.fract_lt_one, Filter.univ_mem, Icc_mem_nhds
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
inst_7 : TopologicalSpace γ
s : β → α
f : β → α → γ
h : ContinuousOn (uncurry f) (SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1))
hs : Continuous[inst_6, inst_3] s
hf : ∀ (s : β), f s 0 = f s 1
⊢ Continuous[inst_6, inst_7] fun (x : β) ↦ f x (fract (s x))

Tactic:
(h.comp_fract' hf).comp (continuous_id.prodMk hs)

Premises used: Continuous.comp, ContinuousOn.comp_fract', continuous_id, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderTopology α
inst_6 : TopologicalSpace β
f : α → β
h : ContinuousOn f (Icc 0 1)
hf : f 0 = f 1
⊢ Continuous[inst_3, inst_6] (f ∘ fract)

Tactic:
ContinuousOn.comp_fract (h.comp continuousOn_snd fun _x hx => (mem_prod.mp hx).2) continuous_id
    fun _ => hf

Premises used: ContinuousOn.comp, continuousOn_snd, Set.mem_prod, continuous_id, And.right, Iff.mp, ContinuousOn.comp_fract
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)

Tactic:
have h := isCoboundedUnder_le_add h₄ h₂
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)

Tactic:
have h' := isBoundedUnder_le_add h₃ h₁
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)

Tactic:
rw [add_comm] at h h'

Premises used: add_comm
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
h₅ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)

Tactic:
rw [add_comm] at h h'

Premises used: add_comm
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
⊢ limsup u f + liminf v f ≤ limsup (u + v) f

Tactic:
add_le_of_forall_lt fun a a_u b b_v ↦ (le_limsup_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, add_le_of_forall_lt, Filter.le_limsup_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
refine :
  ∀ (a : α) (a_u : a < limsup u f) (b : α) (b_v : b < liminf v f) (c : α) (c_ab : c < a + b),
    ∃ᶠ (a : ι) in f, c < (u + v) a
⊢ limsup u f + liminf v f ≤ limsup (u + v) f

Tactic:
refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_limsup_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, add_le_of_forall_lt, Filter.le_limsup_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a < limsup u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
⊢ ∃ᶠ (a : ι) in f, c < (u + v) a

Tactic:
((frequently_lt_of_lt_limsup h₂ a_u).and_eventually
    (eventually_lt_of_lt_liminf b_v h₄)).mono fun _ ab_x ↦ ?_

Premises used: Filter.eventually_lt_of_lt_liminf, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_lt_of_lt_limsup
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a < limsup u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
refine : ∀ (x : ι) (ab_x : a < u x ∧ b < v x), c < (u + v) x
⊢ ∃ᶠ (a : ι) in f, c < (u + v) a

Tactic:
refine ((frequently_lt_of_lt_limsup h₂ a_u).and_eventually
    (eventually_lt_of_lt_liminf b_v h₄)).mono fun _ ab_x ↦ ?_

Premises used: Filter.eventually_lt_of_lt_liminf, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_lt_of_lt_limsup