Theorem: Asymptotics.isLittleO_const_snd_atBot (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✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Tactic:
refine lx.eq_or_neBot.casesOn (fun h ↦ by simp [h]) (fun _ ↦ ?_)
State after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd

State before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Tactic:
show ((fun _ ↦ c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)
State after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)

State before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)
Tactic:
rewrite [← isLittleO_map, map_snd_prod]
State after:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atBot] id

State before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atBot] id
Tactic:
exact isLittleO_const_id_atBot2 c
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
h : lx = ⊥
⊢ (fun x => c) =o[lx ×ˢ atBot] Prod.snd
Tactic:
simp [h]
State after:
no goals