Theorem: Asymptotics.isBigO_rev_of_isBigOUniformly_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✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
⊢ g =O[l] fun x => f (i, x)
Tactic:
obtain ⟨C, hC⟩ := h.bound
State after:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
⊢ g =O[l] fun x => f (i, x)

State before:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
⊢ g =O[l] fun x => f (i, x)
Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem
State after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
⊢ g =O[l] fun x => f (i, x)

State before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
⊢ g =O[l] fun x => f (i, x)
Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ g =O[l] fun x => f (i, x)

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ g =O[l] fun x => f (i, x)
Tactic:
refine isBigO_iff.mpr ⟨C, Filter.eventually_iff_exists_mem.mpr ⟨v, hv, ?_⟩⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ y ∈ v, ‖g y‖ ≤ C * ‖f (i, y)‖

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ y ∈ v, ‖g y‖ ≤ C * ‖f (i, y)‖
Tactic:
exact fun y hy ↦ ht (i, y) <| huv ⟨hu hi, hy⟩
State after:
no goals