-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_rev_principal
    (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) :
    IsBigOWith (‖c‖ / sInf (Norm.norm '' (f '' s))) (𝓟 s) (fun _ => c) f

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (f '' s))
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < (fun a => ‖a‖) (f x)

Tactic:
exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' (f '' s)))

Tactic:
have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' (f '' s)))

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
⊢ 0 < sInf (Norm.norm '' (f '' s))

Tactic:
obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (f '' s))
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < sInf (Norm.norm '' (f '' s))

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
⊢ IsBigOWith (‖c‖ / sInf (Norm.norm '' (f '' s))) (𝓟 s) (fun x => c) f

Tactic:
refine isBigOWith_principal.mpr fun x hx ↦ ?_

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' (f '' s)) * ‖f x‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' (f '' s)) * ‖f x‖

Tactic:
rw [mul_comm_div]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' (f '' s)))

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' (f '' s)))

Tactic:
refine le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
  h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
⊢ 0 < sInf (Norm.norm '' (f '' s))

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (f '' s))
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < sInf (Norm.norm '' (f '' s))

Tactic:
rw [← hnormCx, ← hCx]

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (f '' s)) (sInf ((fun a => ‖a‖) '' (f '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (f '' s))
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < (fun a => ‖a‖) (f x)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' (f '' s)))

Tactic:
replace hs := hs.image_of_continuousOn hf |>.image continuous_norm

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact ((fun a => ‖a‖) '' (f '' s))
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' (f '' s)))