-- 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 inl
ι : 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
⊢ limsup (fun i => f i - c) ⊥ = limsup f ⊥ - c

Tactic:
have {a : R} : sInf Set.univ ≤ a := by
  apply csInf_le _ (Set.mem_univ a)
  simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
  rcases cobdd with ⟨x, hx⟩
  refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
  simp only [Set.mem_univ, hx y, implies_true]

Result:
case inl
ι : 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
this : ∀ {a : R}, sInf Set.univ ≤ a
⊢ limsup (fun i => f i - c) ⊥ = limsup f ⊥ - c

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
⊢ BddBelow Set.univ

Tactic:
simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd

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
a : R
cobdd : ∃ b, ∀ (a : R), b ≤ a
⊢ BddBelow Set.univ

Proof state:
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
y : R
⊢ y ∈ Set.univ → x ≤ y

Tactic:
simp only [Set.mem_univ, hx y, implies_true]

Result:
no goals

Proof state:
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

Tactic:
refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩

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
y : R
⊢ y ∈ Set.univ → x ≤ y

Proof state:
case inl
ι : 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
this : ∀ {a : R}, sInf Set.univ ≤ a
⊢ limsup (fun i => f i - c) ⊥ = limsup f ⊥ - c

Tactic:
simp only [limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]

Result:
case inl
ι : 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
this : ∀ {a : R}, sInf Set.univ ≤ a
⊢ sInf Set.univ = sInf Set.univ - c

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
⊢ limsup (fun i => f i - c) F = limsup f F - c

Tactic:
rcases F.eq_or_neBot with rfl | _

Result:
case inl
ι : 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
⊢ limsup (fun i => f i - c) ⊥ = limsup f ⊥ - c

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

Proof state:
case inl
ι : 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
this : ∀ {a : R}, sInf Set.univ ≤ a
⊢ sInf Set.univ = sInf Set.univ - c

Tactic:
exact this.antisymm (tsub_le_iff_right.2 this)

Result:
no goals

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
⊢ Monotone fun x => x - c

Tactic:
exact fun _ _ h ↦ tsub_le_tsub_right h c

Result:
no goals