Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev (PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Uniformly.lean)

State before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
⊢ IsBigOWith (‖c‖ / sInf (norm '' (C '' s))) (𝓟 s ×ˢ l) (fun x => c) fun x =>
    match x with
    | (i, _x) => C i
Tactic:
refine isBigOWith_iff.mpr <| eventually_of_mem ?_ (fun x hx ↦ ?_) (U := s ×ˢ Set.univ)
State after:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
⊢ s ×ˢ Set.univ ∈ 𝓟 s ×ˢ l

case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ / sInf (norm '' (C '' s)) *
      ‖match x with
        | (i, _x) => C i‖

State before:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
⊢ s ×ˢ Set.univ ∈ 𝓟 s ×ˢ l
Tactic:
exact prod_mem_prod (mem_principal_self s) univ_mem
State after:
no goals

State before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ / sInf (norm '' (C '' s)) *
      ‖match x with
        | (i, _x) => C i‖
Tactic:
rewrite [mul_comm_div]
State after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))

State before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hs : IsCompact s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Tactic:
replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
State after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))

State before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))
Tactic:
have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x.1, hx.1⟩
State after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' s)))

State before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖c‖ ≤
    ‖c‖ *
      (‖match x with
          | (i, _x) => C i‖ /
        sInf (norm '' (C '' 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.1
State after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ 0 < sInf (norm '' (C '' s))

State before:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
⊢ 0 < sInf (norm '' (C '' s))
Tactic:
obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty
State after:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < sInf (norm '' (C '' s))

State before:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < sInf (norm '' (C '' s))
Tactic:
rewrite [← hnormCx, ← hCx]
State after:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < (fun a => ‖a‖) (C x)

State before:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < (fun a => ‖a‖) (C x)
Tactic:
exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)
State after:
no goals