Theorem: Asymptotics.isLittleO_const_fst_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
ly : Filter E
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Tactic:
refine ly.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
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst

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
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Tactic:
show ((fun _ ↦ c) ∘ Prod.fst) =o[atBot ×ˢ ly] (id ∘ Prod.fst)
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
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atBot ×ˢ ly] (id ∘ Prod.fst)

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
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atBot ×ˢ ly] (id ∘ Prod.fst)
Tactic:
rewrite [← isLittleO_map, map_fst_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
ly : Filter E
x✝ : ly.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
ly : Filter E
x✝ : ly.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
ly : Filter E
h : ly = ⊥
⊢ (fun x => c) =o[atBot ×ˢ ly] Prod.fst
Tactic:
simp [h]
State after:
no goals