Theorem: SchwartzMap.tendsto_atTop_zero_real (ForML/SchwartzFourier.lean)

State before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => f x) Filter.atTop (nhds 0)
Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
State after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)

State before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Tactic:
rcases f.decay₁ 1 0 with ⟨C, hC⟩
State after:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + ‖x‖) ^ 1 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)

State before:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + ‖x‖) ^ 1 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Tactic:
simp at hC
State after:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)

State before:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le (h := fun x => C * (1 + |x|)⁻¹) tendsto_const_nhds ?_ ?_ ?_
State after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)

case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹

State before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)

case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
. rw [← mul_zero C]
  refine Filter.Tendsto.const_mul C ?_
  refine Filter.Tendsto.inv_tendsto_atTop ?_
  refine Filter.tendsto_atTop_add_const_left _ 1 ?_
  exact Filter.tendsto_abs_atTop_atTop
State after:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹

State before:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
. intro x
  simp
State after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
. intro x
  simp
  rw [← div_eq_mul_inv]
  rw [le_div_iff (lt_of_lt_of_le zero_lt_one (by simp))]
  rw [mul_comm]
  exact hC x
State after:
no goals

State before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)
Tactic:
rw [← mul_zero C]
State after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds (C * 0))

State before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds (C * 0))
Tactic:
refine Filter.Tendsto.const_mul C ?_
State after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => (1 + |k|)⁻¹) Filter.atTop (nhds 0)

State before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => (1 + |k|)⁻¹) Filter.atTop (nhds 0)
Tactic:
refine Filter.Tendsto.inv_tendsto_atTop ?_
State after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => 1 + |k|) Filter.atTop Filter.atTop

State before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => 1 + |k|) Filter.atTop Filter.atTop
Tactic:
refine Filter.tendsto_atTop_add_const_left _ 1 ?_
State after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => |k|) Filter.atTop Filter.atTop

State before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => |k|) Filter.atTop Filter.atTop
Tactic:
exact Filter.tendsto_abs_atTop_atTop
State after:
no goals

State before:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖
Tactic:
intro x
State after:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => 0) x ≤ (fun x => ‖f x‖) x

State before:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => 0) x ≤ (fun x => ‖f x‖) x
Tactic:
simp
State after:
no goals

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
intro x
State after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => ‖f x‖) x ≤ (fun x => C * (1 + |x|)⁻¹) x

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => ‖f x‖) x ≤ (fun x => C * (1 + |x|)⁻¹) x
Tactic:
simp
State after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C * (1 + |x|)⁻¹

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C * (1 + |x|)⁻¹
Tactic:
rw [← div_eq_mul_inv]
State after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C / (1 + |x|)

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C / (1 + |x|)
Tactic:
rw [le_div_iff (lt_of_lt_of_le zero_lt_one (by simp))]
State after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ * (1 + |x|) ≤ C

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ * (1 + |x|) ≤ C
Tactic:
rw [mul_comm]
State after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (1 + |x|) * ‖f x‖ ≤ C

State before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (1 + |x|) * ‖f x‖ ≤ C
Tactic:
exact hC x
State after:
no goals

State before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ 1 ≤ 1 + |x|
Tactic:
simp
State after:
no goals