-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
/-- `limsup (xᵢ - c) = (limsup xᵢ) - c`. -/
lemma limsup_sub_const (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R]
    (f : ι → R) (c : R)
    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
    Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c

Proof state:
case inr
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
h✝ : F.NeBot
⊢ limsup (fun i => f i - c) F = limsup f F - c

Tactic:
apply (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) _ _).symm

Result:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
h✝ : F.NeBot
⊢ Monotone fun x => x - c

ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
h✝ : F.NeBot
⊢ ContinuousAt (fun x => x - c) (map f F).limsSup

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ f
a : R
⊢ sInf Set.univ ≤ a

Tactic:
apply csInf_le _ (Set.mem_univ a)

Result:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ f
a : R
⊢ BddBelow Set.univ

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
h✝ : F.NeBot
⊢ ContinuousAt (fun x => x - c) (map f F).limsSup

Tactic:
exact (continuous_sub_right c).continuousAt

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ f
a : R
cobdd : ∃ b, ∀ (a : R), b ≤ a
⊢ BddBelow Set.univ

Tactic:
rcases cobdd with ⟨x, hx⟩

Result:
case intro
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ f
a x : R
hx : ∀ (a : R), x ≤ a
⊢ BddBelow Set.univ