awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
⊢ Tendsto g l (𝓝 0)
have refine : ∀ (ε : ℝ) (hε0 : 0 < ε), ∀ᶠ (x : α) in l, Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
Tactic: refine Metric.nhds_basis_closedBall.tendsto_right_iff.mpr fun ε hε0 ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
⊢ ∀ᶠ (x : α) in l, Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
have h : ∀ (x : α) (hfgc : ‖f x • g x‖ ≤ c) (hεf : c / ε ≤ ‖f x‖) (hf0 : f x ≠ 0),
  Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
Tactic: filter_upwards [hc, hasBasis_cobounded_norm.tendsto_right_iff.mp hf (c / ε) trivial,
    hf.eventually_ne_cobounded 0] with x hfgc hεf hf0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
⊢ Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
have h : ∀ (hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ 0) (hfgc : ‖f x • g x‖ ≤ 0) (hεf : 0 / ε ≤ ‖f x‖),
  Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
Tactic: rcases eq_or_lt_of_le ((norm_nonneg _).trans hfgc) with rfl | hc0
Cleared hypotheses: c, hc, hfgc, hεf
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
h :
  ∀ (hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ 0) (hfgc : ‖f x • g x‖ ≤ 0) (hεf : 0 / ε ≤ ‖f x‖),
    Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
⊢ Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
have h₁ : ∀ (hc0 : 0 < c), Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
Tactic: rcases eq_or_lt_of_le ((norm_nonneg _).trans hfgc) with rfl | hc0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ ‖g x‖ ≤ c / ‖f x‖
have rwa : ∀ (hfgc : ‖f x‖ * ‖g x‖ ≤ c) (hεf : c / ε ≤ ‖f x‖) (hf0 : f x ≠ 0) (hc0 : 0 < c), ‖g x‖ ≤ c / ‖f x‖
Tactic: rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
Cleared hypotheses: hfgc, hεf, hf0, hc0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
rwa : ∀ (hfgc : ‖f x‖ * ‖g x‖ ≤ c) (hεf : c / ε ≤ ‖f x‖) (hf0 : f x ≠ 0) (hc0 : 0 < c), ‖g x‖ ≤ c / ‖f x‖
⊢ ‖g x‖ ≤ c / ‖f x‖
have rwa₁ : ∀ (hfgc : ‖g x‖ ≤ c / ‖f x‖) (hεf : c / ε ≤ ‖f x‖) (hf0 : f x ≠ 0) (hc0 : 0 < c), ‖g x‖ ≤ c / ‖f x‖
Tactic: rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
Cleared hypotheses: hfgc, hεf, hf0, hc0
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ c / ‖f x‖ ≤ c / (c / ε)
have hc₁ : 0 ≤ c
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
hc₁ : 0 ≤ c
⊢ c / ‖f x‖ ≤ c / (c / ε)
have hd : 0 < c / ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
have _ : dist (g x) 0 = ‖g x‖
Tactic: calc
    _ = ‖g x‖ := by simp
    _ ≤ c / ‖f x‖ := by rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
    _ ≤ c / (c / ε) := by gcongr
    _ = ε := div_div_cancel₀ hc0.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
_ : dist (g x) 0 = ‖g x‖
⊢ Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
have _₁ : ‖g x‖ ≤ c / ‖f x‖
Tactic: calc
    _ = ‖g x‖ := by simp
    _ ≤ c / ‖f x‖ := by rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
    _ ≤ c / (c / ε) := by gcongr
    _ = ε := div_div_cancel₀ hc0.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
_ : dist (g x) 0 = ‖g x‖
_₁ : ‖g x‖ ≤ c / ‖f x‖
⊢ Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
have _₂ : c / ‖f x‖ ≤ c / (c / ε)
Tactic: calc
    _ = ‖g x‖ := by simp
    _ ≤ c / ‖f x‖ := by rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
    _ ≤ c / (c / ε) := by gcongr
    _ = ε := div_div_cancel₀ hc0.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun (x : α) ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun (x : α) ↦ f₂ x • g x) l (𝓝 t)
have apply : Tendsto (β := ℝ) (fun (x : α) ↦ dist (f₁ x • g x) (f₂ x • g x)) l (𝓝 0)
Tactic: apply hmul.congr_dist
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun (x : α) ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ dist (f₁ x • g x) (f₂ x • g x)) l (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : α) ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)
Tactic: simp_rw [dist_eq_norm, ← sub_smul, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun (x : α) ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)
have hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (comp (β := ℝ) norm fun (x : α) ↦ ‖f₁ x - f₂ x‖)
Tactic: apply isBoundedUnder_le_mul_tendsto_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun (x : α) ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f₁ x - f₂ x‖
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (comp (β := ℝ) norm fun (x : α) ↦ ‖f₁ x - f₂ x‖)
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)
have hg : Tendsto (β := ℝ) (fun (x : α) ↦ ‖g x‖) l (𝓝 0)
Tactic: apply isBoundedUnder_le_mul_tendsto_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun (x : α) ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖g x‖) l (𝓝 0)
have hg : Tendsto g l (𝓝 0)
Tactic: rw [← tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
inst_6 : NormSMulClass ℤ K
inst_7 : LinearOrder K
inst_8 : IsStrictOrderedRing K
inst_9 : FloorSemiring K
inst_10 : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun (n : ℕ) ↦ n • g n) atTop (𝓝 t)
⊢ Tendsto (fun (x : K) ↦ x • g ⌊x⌋₊) atTop (𝓝 t)
have hg₁ : Tendsto (fun (n : ℕ) ↦ HSMul.hSMul.{u_5, u_4, u_4} (α := K) (↑n : K) (g n)) atTop (𝓝 t)
Tactic: replace hg : Tendsto (fun n : ℕ ↦ (n : K) • g n) atTop (𝓝 t) := mod_cast hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
inst_6 : NormSMulClass ℤ K
inst_7 : LinearOrder K
inst_8 : IsStrictOrderedRing K
inst_9 : FloorSemiring K
inst_10 : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun (n : ℕ) ↦ HSMul.hSMul.{u_5, u_4, u_4} (α := K) (↑n : K) (g n)) atTop (𝓝 t)
⊢ Tendsto (fun (x : K) ↦ x • g ⌊x⌋₊) atTop (𝓝 t)
have hf₁ : Tendsto (fun (x : K) ↦ (↑⌊x⌋₊ : K)) atTop (cobounded K)
Tactic: apply tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder
    (hg.comp tendsto_nat_floor_atTop)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
inst_6 : NormSMulClass ℤ K
inst_7 : LinearOrder K
inst_8 : IsStrictOrderedRing K
inst_9 : FloorSemiring K
inst_10 : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun (n : ℕ) ↦ HSMul.hSMul.{u_5, u_4, u_4} (α := K) (↑n : K) (g n)) atTop (𝓝 t)
hf₁ : Tendsto (fun (x : K) ↦ (↑⌊x⌋₊ : K)) atTop (cobounded K)
⊢ Tendsto (fun (x : K) ↦ x • g ⌊x⌋₊) atTop (𝓝 t)
have hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : K) ↦ ‖(↑⌊x⌋₊ : K) - x‖
Tactic: apply tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder
    (hg.comp tendsto_nat_floor_atTop)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
inst_6 : NormSMulClass ℤ K
inst_7 : LinearOrder K
inst_8 : IsStrictOrderedRing K
inst_9 : FloorSemiring K
inst_10 : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun (n : ℕ) ↦ HSMul.hSMul.{u_5, u_4, u_4} (α := K) (↑n : K) (g n)) atTop (𝓝 t)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : K) ↦ ‖(↑⌊x⌋₊ : K) - x‖
have hbdd : ∀ᶠ (x : K) in atTop, ‖(↑⌊x⌋₊ : K) - x‖ ≤ norm.{u_5} (E := K) 1
Tactic: apply isBoundedUnder_of_eventually_le (a := ‖(1 : K)‖)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
inst_6 : NormSMulClass ℤ K
inst_7 : LinearOrder K
inst_8 : IsStrictOrderedRing K
inst_9 : FloorSemiring K
inst_10 : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun (n : ℕ) ↦ HSMul.hSMul.{u_5, u_4, u_4} (α := K) (↑n : K) (g n)) atTop (𝓝 t)
⊢ ∀ᶠ (x : K) in atTop, ‖(↑⌊x⌋₊ : K) - x‖ ≤ norm.{u_5} (E := K) 1
have apply : ∀ᶠ (x : K) in atTop, |(↑⌊x⌋₊ : K) - x| ≤ |1|
Tactic: apply Eventually.mono _ (fun x h ↦ norm_le_norm_of_abs_le_abs h)
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
n : ℕ
hn : n ≠ 0
⊢ h.lim ≤ u n / (↑n : ℝ)
have rw : sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) ≤ u n / (↑n : ℝ)
Tactic: rw [Subadditive.lim]
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u (0 * n + r) ≤ (↑0 : ℝ) * u n + u r
have zero : u r ≤ u r
Tactic: simp only [Nat.cast_zero, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ u ((k + 1) * n + r) = u (n + (k * n + r))
have e_a : (k + 1) * n + r = n + (k * n + r)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ u n + u (k * n + r) ≤ u n + ((↑k : ℝ) * u n + u r)
have grw : u n + ((↑k : ℝ) * u n + u r) ≤ u n + ((↑k : ℝ) * u n + u r)
Tactic: grw [IH]
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ u n + ((↑k : ℝ) * u n + u r) = (↑(k + 1) : ℝ) * u n + u r
have simp : u n + ((↑k : ℝ) * u n + u r) = HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * u n + u r
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ u ((k + 1) * n + r) ≤ (↑(k + 1) : ℝ) * u n + u r
have u₁ : u ((k + 1) * n + r) = u (n + (k * n + r))
Tactic: calc
      u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
      _ ≤ u n + u (k * n + r) := h _ _
      _ ≤ u n + (k * u n + u r) := by grw [IH]
      _ = (k + 1 : ℕ) * u n + u r := by simp; ring
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
u₁ : u ((k + 1) * n + r) = u (n + (k * n + r))
⊢ u ((k + 1) * n + r) ≤ (↑(k + 1) : ℝ) * u n + u r
have u₂ : u n + u (k * n + r) ≤ u n + ((↑k : ℝ) * u n + u r)
Tactic: calc
      u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
      _ ≤ u n + u (k * n + r) := h _ _
      _ ≤ u n + (k * u n + u r) := by grw [IH]
      _ = (k + 1 : ℕ) * u n + u r := by simp; ring
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
u₁ : u ((k + 1) * n + r) = u (n + (k * n + r))
u₂ : u n + u (k * n + r) ≤ u n + ((↑k : ℝ) * u n + u r)
⊢ u ((k + 1) * n + r) ≤ (↑(k + 1) : ℝ) * u n + u r
have u₃ : u n + ((↑k : ℝ) * u n + u r) = (↑(k + 1) : ℝ) * u n + u r
Tactic: calc
      u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
      _ ≤ u n + u (k * n + r) := h _ _
      _ ≤ u n + (k * u n + u r) := by grw [IH]
      _ = (k + 1 : ℕ) * u n + u r := by simp; ring
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ (↑k : ℝ) * u n + u r
have zero : u (0 * n + r) ≤ (↑0 : ℝ) * u n + u r
Tactic: induction k with
  | zero => simp only [Nat.cast_zero, zero_mul, zero_add]; rfl
  | succ k IH =>
    calc
      u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
      _ ≤ u n + u (k * n + r) := h _ _
      _ ≤ u n + (k * u n + u r) := by grw [IH]
      _ = (k + 1 : ℕ) * u n + u r := by simp; ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
zero : u (0 * n + r) ≤ (↑0 : ℝ) * u n + u r
⊢ u (k * n + r) ≤ (↑k : ℝ) * u n + u r
have succ : ∀ (k : ℕ) (IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r), u ((k + 1) * n + r) ≤ (↑(k + 1) : ℝ) * u n + u r
Tactic: induction k with
  | zero => simp only [Nat.cast_zero, zero_mul, zero_add]; rfl
  | succ k IH =>
    calc
      u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
      _ ≤ u n + u (k * n + r) := h _ _
      _ ≤ u n + (k * u n + u r) := by grw [IH]
      _ = (k + 1 : ℕ) * u n + u r := by simp; ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / (↑p : ℝ) < L
have refine : ∀ r < n, ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L
Tactic: refine .atTop_of_arithmetic hn fun r _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (hypothesis)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L
have A : Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
  (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
Tactic: have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
    (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
      (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <| by simpa
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (hypothesis)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
⊢ Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
have A₁ : Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop (𝓝 (u n / (↑n : ℝ)))
Tactic: rw [add_zero, add_zero] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A : Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop (𝓝 (u n / (↑n : ℝ)))
⊢ Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
have refine : ∀ (x : ℝ) (hx : x ≠ 0),
  (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x) = (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) x
Tactic: refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (hypothesis)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L
have B : Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
Tactic: have B : Tendsto (fun x => (x * u n + u r) / (x * n + r)) atTop (𝓝 (u n / n)) := by
    rw [add_zero, add_zero] at A
    refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
    simp only [add_div' _ _ _ hx, div_div_div_cancel_right₀ hx, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
B : Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L
have refine : ∀ (k : ℕ) (hk : ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k < L),
  u (n * k + r) / (↑(n * k + r) : ℝ) < L
Tactic: refine ((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk => ?_
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
B : Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
k : ℕ
hk : ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k < L
⊢ u (n * k + r) / (↑(n * k + r) : ℝ) < L
have rw : u (k * n + r) / (↑(k * n + r) : ℝ) < L
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
B : Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
k : ℕ
hk : ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k < L
⊢ u (k * n + r) / (↑(k * n + r) : ℝ) < L
have refine : u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k
Tactic: refine lt_of_le_of_lt ?_ hk