awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
ε : ℝ
hε0 : 0 < ε
x : α
hf0 : f x ≠ 0
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:
simpa [(smul_eq_zero_iff_right hf0).mp (norm_le_zero_iff.mp hfgc)] using hε0.le

Premises used: LT.lt.le, smul_eq_zero_iff_right, norm_le_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ 0 < ‖f x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hfgc : ‖g x‖ ≤ c / ‖f x‖) (hεf : c / ε ≤ ‖f x‖) (hf0 : f x ≠ 0) (hc0 : 0 < c), ‖g x‖ ≤ c / ‖f x‖
⊢ ‖g x‖ ≤ c / ‖f x‖

Tactic:
rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc

Premises used: le_div_iff₀', norm_smul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
hd : 0 < c / ε
⊢ c / ‖f x‖ ≤ c / (c / ε)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 / (c / ε) = ε

Tactic:
div_div_cancel₀ hc0.ne'

Premises used: LT.lt.ne', div_div_cancel₀
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
_₂ : c / ‖f x‖ ≤ c / (c / ε)
⊢ Membership.mem (γ := Set R) (closedBall 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'

Premises used: HDiv.hDiv, LT.lt.ne', div_div_cancel₀
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
apply : Tendsto (β := ℝ) (fun (x : α) ↦ dist (f₁ x • g x) (f₂ x • g x)) l (𝓝 0)
⊢ Tendsto (fun (x : α) ↦ f₂ x • g x) l (𝓝 t)

Tactic:
apply hmul.congr_dist

Premises used: Filter.Tendsto.congr_dist
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
simp_rw : Tendsto (β := ℝ) (fun (x : α) ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ dist (f₁ x • g x) (f₂ x • g x)) l (𝓝 0)

Tactic:
simp_rw [dist_eq_norm, ← sub_smul, norm_smul]

Premises used: dist_eq_norm, norm_smul, sub_smul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖)
hg : Tendsto (β := ℝ) (fun (x : α) ↦ ‖g x‖) l (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)

Tactic:
apply isBoundedUnder_le_mul_tendsto_zero

Premises used: Filter.isBoundedUnder_le_mul_tendsto_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ comp (β := ℝ) norm (fun (x : α) ↦ ‖f₁ x - f₂ x‖) x

Tactic:
simpa using hbdd
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖g x‖) l (𝓝 0)

Tactic:
rw [← tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 g l (𝓝 0)

Tactic:
tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hmul.norm.isBoundedUnder_le hf₁

Premises used: Filter.Tendsto.isBoundedUnder_le, tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded, Filter.Tendsto.norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 g l (𝓝 0)

Tactic:
exact tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hmul.norm.isBoundedUnder_le hf₁

Premises used: Filter.Tendsto.isBoundedUnder_le, tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded, Filter.Tendsto.norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 (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
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
hbdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : K) ↦ ‖(↑⌊x⌋₊ : K) - x‖
⊢ Tendsto (fun (x : K) ↦ x • g ⌊x⌋₊) atTop (𝓝 t)

Tactic:
apply tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder
    (hg.comp tendsto_nat_floor_atTop)

Premises used: tendsto_nat_floor_atTop, tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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⌋₊ : K)) atTop (cobounded K)

Tactic:
tendsto_natCast_atTop_cobounded.comp tendsto_nat_floor_atTop

Premises used: tendsto_nat_floor_atTop, Filter.Tendsto.comp, tendsto_natCast_atTop_cobounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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⌋₊ : K)) atTop (cobounded K)

Tactic:
exact tendsto_natCast_atTop_cobounded.comp tendsto_nat_floor_atTop

Premises used: tendsto_nat_floor_atTop, Filter.Tendsto.comp, tendsto_natCast_atTop_cobounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
hbdd : ∀ᶠ (x : K) in atTop, ‖(↑⌊x⌋₊ : K) - x‖ ≤ norm.{u_5} (E := K) 1
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : K) ↦ ‖(↑⌊x⌋₊ : K) - x‖

Tactic:
apply isBoundedUnder_of_eventually_le (a := ‖(1 : K)‖)

Premises used: Filter.isBoundedUnder_of_eventually_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
apply : ∀ᶠ (x : K) in atTop, |(↑⌊x⌋₊ : K) - x| ≤ |1|
⊢ ∀ᶠ (x : K) in atTop, ‖(↑⌊x⌋₊ : K) - x‖ ≤ norm.{u_5} (E := K) 1

Tactic:
apply Eventually.mono _ (fun x h ↦ norm_le_norm_of_abs_le_abs h)

Premises used: norm_le_norm_of_abs_le_abs, Filter.Eventually.mono
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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| ≤ |1|

Tactic:
simpa using ⟨0, fun _ h ↦ mod_cast Nat.abs_floor_sub_le h⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : NormedRing R
inst_2 : Module K R
inst_3 : IsTorsionFree K R
inst_4 : NormSMulClass K R
inst_5 : NormSMulClass ℤ K
inst_6 : LinearOrder K
inst_7 : IsStrictOrderedRing K
inst_8 : FloorSemiring K
inst_9 : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun (n : ℕ) ↦ (↑n : R) * g n) atTop (𝓝 t)
⊢ Tendsto (fun (n : ℕ) ↦ n • g n) atTop (𝓝 t)

Tactic:
simpa only [nsmul_eq_mul] using hg

Premises used: nsmul_eq_mul
-- Module: Mathlib.Analysis.SpecificLimits.RCLike
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Tendsto ofReal (Bornology.cobounded ℝ) (Bornology.cobounded 𝕜)

Tactic:
tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_norm_cobounded_atTop)

Premises used: Real, congrArg, RCLike.norm_ofReal, cast, Filter.atTop, funext, Filter.Tendsto, Iff.mp, tendsto_norm_cobounded_atTop, Bornology.cobounded, tendsto_norm_atTop_iff_cobounded, congrFun', Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.RCLike
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Tendsto ofReal atTop (Bornology.cobounded 𝕜)

Tactic:
tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_abs_atTop_atTop)

Premises used: congrArg, RCLike.norm_ofReal, cast, Filter.atTop, funext, Filter.Tendsto, Iff.mp, tendsto_norm_atTop_iff_cobounded, congrFun', Eq.symm, Filter.tendsto_abs_atTop_atTop
-- Module: Mathlib.Analysis.SpecificLimits.RCLike
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Tendsto ofReal atBot (Bornology.cobounded 𝕜)

Tactic:
tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_abs_atBot_atTop)

Premises used: congrArg, RCLike.norm_ofReal, cast, Filter.tendsto_abs_atBot_atTop, Filter.atTop, funext, Filter.Tendsto, Iff.mp, Filter.atBot, tendsto_norm_atTop_iff_cobounded, congrFun', Eq.symm
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
n : ℕ
hn : n ≠ 0
rw : sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) ≤ u n / (↑n : ℝ)
⊢ h.lim ≤ u n / (↑n : ℝ)

Tactic:
rw [Subadditive.lim]

Premises used: Subadditive.lim
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) ≤ u n / (↑n : ℝ)

Tactic:
csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩

Premises used: Set.image_subset_range, BddBelow.mono, And.intro, Exists.intro, csInf_le, rfl, Ne.bot_lt
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) ≤ u n / (↑n : ℝ)

Tactic:
exact csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩

Premises used: Set.image_subset_range, BddBelow.mono, And.intro, Exists.intro, csInf_le, rfl, Ne.bot_lt
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
zero : u r ≤ u r
⊢ u (0 * n + r) ≤ (↑0 : ℝ) * u n + u r

Tactic:
simp only [Nat.cast_zero, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add, Nat.cast_zero
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u r ≤ u r

Tactic:
rfl
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
e_a : (k + 1) * n + r = n + (k * n + r)
⊢ u ((k + 1) * n + r) = u (n + (k * n + r))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ (k + 1) * n + r = n + (k * n + r)

Tactic:
ring
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ u (n + (k * n + r)) ≤ u n + u (k * n + r)

Tactic:
h _ _
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
grw grw₁ : u n + ((↑k : ℝ) * u n + u r) ≤ u n + ((↑k : ℝ) * u n + u r)
⊢ u n + u (k * n + r) ≤ u n + ((↑k : ℝ) * u n + u r)

Tactic:
grw [IH]
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
simp : u n + ((↑k : ℝ) * u n + u r) = HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * u n + u r
⊢ u n + ((↑k : ℝ) * u n + u r) = (↑(k + 1) : ℝ) * u n + u r

Tactic:
simp
-- Module: Mathlib.Analysis.Subadditive
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) = HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * u n + u r

Tactic:
ring
-- Module: Mathlib.Analysis.Subadditive
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₃ : u n + ((↑k : ℝ) * u n + u r) = (↑(k + 1) : ℝ) * u n + u r
⊢ u ((k + 1) * n + 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

Premises used: HMul.hMul, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
zero : u (0 * n + r) ≤ (↑0 : ℝ) * u n + u r
succ : ∀ (k : ℕ) (IH : u (k * n + r) ≤ (↑k : ℝ) * u n + u r), u ((k + 1) * n + r) ≤ (↑(k + 1) : ℝ) * u n + u r
⊢ u (k * n + r) ≤ (↑k : ℝ) * 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

Premises used: HMul.hMul, MulZeroClass.zero_mul, zero_add, Nat.cast, HAdd.hAdd, Nat.cast_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / (↑p : ℝ) < L

Tactic:
.atTop_of_arithmetic hn fun r _ => ?_

Premises used: Filter.Eventually.atTop_of_arithmetic
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
refine : ∀ r < n, ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / (↑p : ℝ) < L

Tactic:
refine .atTop_of_arithmetic hn fun r _ => ?_
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 0 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
⊢ 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
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop (𝓝 (u n / (↑n : ℝ)))

Tactic:
rw [add_zero, add_zero] at A

Premises used: add_zero
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)))

Tactic:
A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.mono, Filter.Tendsto.congr', OfNat.ofNat
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)))
refine :
  ∀ (x : ℝ) (hx : x ≠ 0),
    (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x) = (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) x
⊢ Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))

Tactic:
refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.mono, Filter.Tendsto.congr', OfNat.ofNat
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)))
x : ℝ
hx : x ≠ 0
⊢ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x) = (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) x

Tactic:
simp only [add_div' _ _ _ hx, div_div_div_cancel_right₀ hx, mul_comm]

Premises used: div_div_div_cancel_right₀, add_div', mul_comm
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)))

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]