-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_principal {s : Set α} : f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Proof state:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
c : ℝ
hc : c ∈ Ioi 0
⊢ (fun x_1 => ‖f'' x‖) c ≤ (fun c => c * ‖g' x‖) c

Tactic:
exact eventually_principal.1 (h hc) x hx

Result:
no goals

Proof state:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
⊢ ‖f'' x‖ ≤ 0

Tactic:
have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
  ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
    inf_le_left

Result:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ ‖f'' x‖ ≤ 0

Proof state:
case refine_2
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ f'' =o[𝓟 s] g'

Tactic:
apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl

Result:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ (fun _x => 0) =ᶠ[𝓟 s] f''

Proof state:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ (fun x_1 => ‖f'' x‖) ≤ᶠ[𝓝[>] 0] fun c => c * ‖g' x‖

Tactic:
apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))

Result:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
c : ℝ
hc : c ∈ Ioi 0
⊢ (fun x_1 => ‖f'' x‖) c ≤ (fun c => c * ‖g' x‖) c

Proof state:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : f'' =o[𝓟 s] g'
x : α
hx : x ∈ s
⊢ ‖f'' x‖ ≤ 0

Tactic:
simp only [isLittleO_iff, isBigOWith_principal] at h

Result:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
⊢ ‖f'' x‖ ≤ 0

Proof state:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ ‖f'' x‖ ≤ 0

Tactic:
apply le_of_tendsto_of_tendsto tendsto_const_nhds this

Result:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ (fun x_1 => ‖f'' x‖) ≤ᶠ[𝓝[>] 0] fun c => c * ‖g' x‖

Proof state:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Tactic:
refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : f'' =o[𝓟 s] g'
x : α
hx : x ∈ s
⊢ ‖f'' x‖ ≤ 0

case refine_2
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ f'' =o[𝓟 s] g'

Proof state:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ (fun _x => 0) =ᶠ[𝓟 s] f''

Tactic:
exact fun x hx ↦ (h x hx).symm

Result:
no goals