Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact (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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
⊢ IsBigOWith (sSup (norm '' (C '' s)) / ‖c‖) (𝓟 s ×ˢ l)
    (fun x =>
      match x with
      | (i, _x) => C i)
    fun x => c
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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s)) / ‖c‖ * ‖c‖

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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s)) / ‖c‖ * ‖c‖
Tactic:
rw [div_mul_cancel₀ _ hc]
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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hs : IsCompact s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Tactic:
have h_sSup := hs.isLUB_sSup <| 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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sSup : IsLUB ((fun a => ‖a‖) '' (C '' s)) (sSup ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (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✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn C s
hc : ‖c‖ ≠ 0
l : Filter α
x : ι × α
hx : x ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sSup : IsLUB ((fun a => ‖a‖) '' (C '' s)) (sSup ((fun a => ‖a‖) '' (C '' s)))
⊢ ‖match x with
      | (i, _x) => C i‖ ≤
    sSup (norm '' (C '' s))
Tactic:
exact h_sSup.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx.1
State after:
no goals