awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
⊢ Tendsto.{0, u_1} (β := K) (fun (n : ℕ) ↦ a * c ^ n / (↑(n - d)! : K)) atTop (𝓝 0)
have rw : (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)) ∧
  ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'
Tactic: rw [tendsto_order]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'
have left : ∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
left : ∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'
have right : ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
⊢ ∀ᶠ (b : ℕ) in atTop, ε < a * c ^ b / (↑(b - d)! : K)
have h : ∀ (n : ℕ) (h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)), ε < a * c ^ n / (↑(n - d)! : K)
Tactic: filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)
⊢ ε < a * c ^ n / (↑(n - d)! : K)
have h₁ : a * c ^ n / ε < (↑(n - d)! : K)
Tactic: rw [mul_right_comm, ← div_eq_mul_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
⊢ ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < ε
have h : ∀ (n : ℕ) (h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)), a * c ^ n / (↑(n - d)! : K) < ε
Tactic: filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)
⊢ a * c ^ n / (↑(n - d)! : K) < ε
have h₁ : a * c ^ n / ε < (↑(n - d)! : K)
Tactic: rw [mul_right_comm, ← div_eq_mul_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * c ^ n / ε < (↑(n - d)! : K)
⊢ ε < a * c ^ n / (↑(n - d)! : K)
have h₁ : (↑(n - d)! : K) * ε < a * c ^ n
Tactic: rw [div_lt_iff_of_neg hε] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n / ε < (↑(n - d)! : K)
⊢ a * c ^ n / (↑(n - d)! : K) < ε
have h₁ : a * c ^ n < (↑(n - d)! : K) * ε
Tactic: rw [div_lt_iff₀ hε] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
c : K
⊢ Tendsto.{0, u_1} (β := K) (fun (n : ℕ) ↦ c ^ n / (↑n ! : K)) atTop (𝓝 0)
have h : ∀ (x : ℕ), c ^ x = 1 * c ^ x
Tactic: convert! tendsto_mul_pow_div_factorial_sub_atTop 1 c 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
c : K
x : ℕ
⊢ c ^ x = 1 * c ^ x
have h : c ^ x = c ^ x
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
⊢ b ≤ floor.{u_1} (α := α) (↑(b + 1) : α)
have rw : b ≤ b + 1
Tactic: rw [floor_intCast]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
⊢ ceil.{u_1} (α := α) (↑(b - 1) : α) ≤ b
have rw : b - 1 ≤ b
Tactic: rw [ceil_intCast]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
⊢ (↑(⌈x⌉ - 1) : α) < x
have rw : (↑⌈x⌉ : α) < x + 1
Tactic: rw [cast_sub, cast_one, sub_lt_iff_lt_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
h₁ : (↑(⌈x⌉ - 1) : α) < x
⊢ x ≤ HAdd.hAdd (α := α) (↑(⌈x⌉ - 1) : α) 1
have rw : x ≤ (↑⌈x⌉ : α)
Tactic: rw [cast_sub, cast_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
x : α
⊢ HSub.hSub (α := α) (↑(⌊x⌋ + 1) : α) 1 ≤ x
have rw : (↑⌊x⌋ : α) ≤ x
Tactic: rw [cast_add, cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] HSub.hSub (α := α) (↑n : α) 1
have rw : LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n - 1))) (𝓝[≤] (↑(n - 1) : α))
Tactic: rw [← @cast_one α, ← cast_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] HAdd.hAdd (α := α) (↑n : α) 1
have rw : LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n + 1))) (𝓝[≥] (↑(n + 1) : α))
Tactic: rw [← @cast_one α, ← cast_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α)) (𝓝 1)
have rw : Tendsto fract (𝓝[<] (↑n : α)) (𝓝 ((↑n : α) - HSub.hSub (α := α) (↑n : α) 1))
Tactic: rw [← sub_sub_cancel (n : α) 1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 fract (𝓝[<] (↑n : α)) (𝓝 ((↑n : α) - HSub.hSub (α := α) (↑n : α) 1))
have refine : Tendsto (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[<] (↑n : α)) (𝓝 (HSub.hSub (α := α) (↑n : α) 1))
Tactic: refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (st : β × α) ↦ f st.1 (fract st.2)
have change : Continuous[instTopologicalSpaceProd, inst_7] (uncurry f ∘ Prod.map id fract)
Tactic: change Continuous (uncurry f ∘ Prod.map id fract)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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
⊢ Continuous[instTopologicalSpaceProd, inst_7] (uncurry f ∘ Prod.map id fract)
have rw : ∀ (x : β × α), ContinuousAt (uncurry f ∘ Prod.map id fract) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
have inl : ∀ (n : ℤ), ContinuousAt (uncurry f ∘ Prod.map id fract) (s, (↑n : α))
Tactic: rcases em (∃ n : ℤ, t = n) with (⟨n, rfl⟩ | ht)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α))
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
have inr : ∀ (ht : ¬∃ (n : ℤ), t = (↑n : α)), ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
Tactic: rcases em (∃ n : ℤ, t = n) with (⟨n, rfl⟩ | ht)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : ℤ
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, (↑n : α))
have 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 : α))))
Tactic: rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α)))) ∧
    Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
      (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
have inl : Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
  (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α)))) ∧
    Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
      (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
have inl₁ : Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
  (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α))))
have inl : SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] 1) ≤ 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 1)
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 ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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)
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[<] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
have inl₁ : 𝓝 (uncurry f (s, 1)) = 𝓝 ((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 ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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) (𝓝[<] 1) ≤ 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 1)
have inl : SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Ico 0 1] 1) ≤ SProd.sprod (β := Filter α) (𝓝 s) (𝓝[Icc 0 1] 1)
Tactic: rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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 : α))))
have inl : SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] 0) = 𝓝[SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1)] (s, 0)
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 ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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)
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (SProd.sprod (β := Filter α) (𝓝 s) (𝓝[≥] (↑n : α)))
    (𝓝 ((uncurry f ∘ Prod.map id fract) (s, (↑n : α))))
have inl₁ : 𝓝 (uncurry f (s, 0)) = 𝓝 ((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 ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (hypothesis)
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 : α)
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
have ht₁ : t ≠ (↑⌊t⌋ : α)
Tactic: replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Floor (goal)
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)
have inr : SProd.sprod (α := Set β) (β := Set α) univ (Icc 0 1) ∈ 𝓝 (Prod.map id fract (s, t))
Tactic: refine (h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ limsup u f + liminf v f ≤ limsup (u + v) f
have h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
Tactic: have h := isCoboundedUnder_le_add h₄ h₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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)
⊢ limsup u f + liminf v f ≤ limsup (u + v) f
have h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (v + u)
Tactic: have h' := isBoundedUnder_le_add h₃ h₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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)
⊢ limsup u f + liminf v f ≤ limsup (u + v) f
have h₅ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
Tactic: rw [add_comm] at h h'
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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)
⊢ limsup u f + liminf v f ≤ limsup (u + v) f
have h'₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
Tactic: rw [add_comm] at h h'
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have 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
Tactic: refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_limsup_iff h h').2 fun c c_ab ↦ ?_