awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddRightMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
x x_1 : R
h : x ≤ x_1
dsimp : x + c ≤ x_1 + c
⊢ LE.le.{u_4} (α := R) ((fun (x : R) ↦ x + c) x) ((fun (x : R) ↦ x + c) x_1)

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddRightMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
x x_1 : R
h : x ≤ x_1
⊢ x + c ≤ x_1 + c

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
inl :
  ∀ (cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f)
    (bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f), limsup (fun (i : ι) ↦ c - f i) ⊥ = c - liminf f ⊥
inr : F.NeBot → limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F

Tactic:
rcases F.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
inl : sInf Set.univ = c - sSup Set.univ
⊢ limsup (fun (i : ι) ↦ c - f i) ⊥ = c - liminf f ⊥

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

Premises used: Filter.limsSup, Filter.limsInf, Filter.map_bot, Filter.liminf, Filter.limsup, Set.setOf_true, Filter.eventually_bot
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
⊢ ∃ (b : R), ∀ (a : R), b ≥ a

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

Premises used: Filter.map_bot, Filter.IsCoboundedUnder, Filter.IsCobounded, true_implies, Filter.eventually_bot
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
cobdd : ∃ (b : R), ∀ (a : R), b ≥ a
inl : ∀ (x : R) (hx : ∀ (a : R), x ≥ a), sInf Set.univ = c - sSup Set.univ
⊢ sInf Set.univ = c - sSup Set.univ

Tactic:
rcases cobdd with ⟨x, hx⟩
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ sInf Set.univ = c - sSup Set.univ

Tactic:
(csInf_le ?_ (Set.mem_univ _)).antisymm
      (tsub_le_iff_tsub_le.1 (le_csSup ?_ (Set.mem_univ _)))

Premises used: LE.le.antisymm, Iff.mp, Set.mem_univ, tsub_le_iff_tsub_le, le_csSup, csInf_le
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
inl : BddBelow.{u_4} (α := R) Set.univ
inl₁ : BddAbove.{u_4} (α := R) Set.univ
⊢ sInf Set.univ = c - sSup Set.univ

Tactic:
refine (csInf_le ?_ (Set.mem_univ _)).antisymm
      (tsub_le_iff_tsub_le.1 (le_csSup ?_ (Set.mem_univ _)))

Premises used: LE.le.antisymm, Iff.mp, Set.mem_univ, tsub_le_iff_tsub_le, le_csSup, csInf_le
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ BddBelow.{u_4} (α := R) Set.univ

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

Premises used: Iff.mpr, HSub.hSub, mem_lowerBounds, Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
inl : ∀ (y : R), Membership.mem (γ := Set R) Set.univ y → x - x ≤ y
⊢ BddBelow.{u_4} (α := R) Set.univ

Tactic:
refine ⟨x - x, mem_lowerBounds.2 fun y ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
inl : x - x ≤ y
⊢ Membership.mem (γ := Set R) Set.univ y → x - x ≤ y

Tactic:
simp only [Set.mem_univ, true_implies]

Premises used: true_implies, Set.mem_univ
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ x - x ≤ y

Tactic:
tsub_le_iff_tsub_le.1 (hx (x - y))

Premises used: HSub.hSub, Iff.mp, tsub_le_iff_tsub_le
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ x - x ≤ y

Tactic:
exact tsub_le_iff_tsub_le.1 (hx (x - y))

Premises used: HSub.hSub, Iff.mp, tsub_le_iff_tsub_le
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ BddAbove.{u_4} (α := R) Set.univ

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

Premises used: Iff.mpr, BddAbove, Set.Nonempty, Exists.intro, mem_upperBounds
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
inl : ∀ (y : R), Membership.mem (γ := Set R) Set.univ y → y ≤ x
⊢ BddAbove.{u_4} (α := R) Set.univ

Tactic:
refine ⟨x, mem_upperBounds.2 fun y ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ Membership.mem (γ := Set R) Set.univ y → y ≤ x

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

Premises used: Set.mem_univ, implies_true
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
h : F.NeBot
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F

Tactic:
(Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt cobdd bdd_below).symm

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Filter.limsup, tsub_le_tsub_left, Continuous.continuousAt, Set.preimage, Eq.symm, continuous_sub_left, Antitone.map_limsInf_of_continuousAt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
inst_7 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
h : F.NeBot
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F

Tactic:
exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt cobdd bdd_below).symm

Premises used: tsub_le_tsub_left, Continuous.continuousAt, Eq.symm, continuous_sub_left, Antitone.map_limsInf_of_continuousAt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
inl :
  ∀ (bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f)
    (cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f), limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c
inr : F.NeBot → limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c

Tactic:
rcases F.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
a : R
apply : BddBelow.{u_4} (α := R) Set.univ
⊢ sInf Set.univ ≤ a

Tactic:
apply csInf_le _ (Set.mem_univ a)

Premises used: Set.mem_univ, csInf_le
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
a : R
⊢ ∃ (b : R), ∀ (a : R), b ≤ a

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

Premises used: Filter.map_bot, Filter.IsCoboundedUnder, Filter.IsCobounded, true_implies, Filter.eventually_bot
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
a : R
cobdd : ∃ (b : R), ∀ (a : R), b ≤ a
rcases : ∀ (x : R) (hx : ∀ (a : R), x ≤ a), BddBelow.{u_4} (α := R) Set.univ
⊢ BddBelow.{u_4} (α := R) Set.univ

Tactic:
rcases cobdd with ⟨x, hx⟩
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
a x : R
hx : ∀ (a : R), x ≤ a
⊢ BddBelow.{u_4} (α := R) Set.univ

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

Premises used: Iff.mpr, mem_lowerBounds, Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
a x : R
hx : ∀ (a : R), x ≤ a
refine : ∀ (y : R), Membership.mem (γ := Set R) Set.univ y → x ≤ y
⊢ BddBelow.{u_4} (α := R) Set.univ

Tactic:
refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
a x : R
hx : ∀ (a : R), x ≤ a
y : R
⊢ Membership.mem (γ := Set R) Set.univ y → x ≤ y

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

Premises used: Set.mem_univ, implies_true
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
⊢ ∀ {a : R}, sInf Set.univ ≤ a

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]
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
this : ∀ {a : R}, sInf Set.univ ≤ a
inl : sInf Set.univ = sInf Set.univ - c
⊢ limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c

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

Premises used: Filter.limsSup, Filter.map_bot, Filter.limsup, Set.setOf_true, Filter.eventually_bot
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
this : ∀ {a : R}, sInf Set.univ ≤ a
⊢ sInf Set.univ = sInf Set.univ - c

Tactic:
this.antisymm (tsub_le_iff_right.2 this)

Premises used: Iff.mpr, LE.le.antisymm, tsub_le_iff_right
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ 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)

Premises used: Iff.mpr, LE.le.antisymm, tsub_le_iff_right
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
h : F.NeBot
apply : Monotone (β := R) fun (x : R) ↦ x - c
apply₁ : ContinuousAt (Y := R) (fun (x : R) ↦ x - c) (map f F).limsSup
⊢ 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

Premises used: Monotone.map_limsSup_of_continuousAt, Eq.symm
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
h : F.NeBot
⊢ Monotone (β := R) fun (x : R) ↦ x - c

Tactic:
fun _ _ h ↦ tsub_le_tsub_right h c

Premises used: Monotone, tsub_le_tsub_right
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
h : F.NeBot
⊢ Monotone (β := R) fun (x : R) ↦ x - c

Tactic:
exact fun _ _ h ↦ tsub_le_tsub_right h c

Premises used: tsub_le_tsub_right
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
h : F.NeBot
⊢ ContinuousAt (Y := R) (fun (x : R) ↦ x - c) (map f F).limsSup

Tactic:
(continuous_sub_right c).continuousAt

Premises used: Continuous.continuousAt, continuous_sub_right
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : AddCommSemigroup R
inst_4 : Sub R
inst_5 : ContinuousSub R
inst_6 : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
h : F.NeBot
⊢ ContinuousAt (Y := R) (fun (x : R) ↦ x - c) (map f F).limsSup

Tactic:
exact (continuous_sub_right c).continuousAt

Premises used: Continuous.continuousAt, continuous_sub_right
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : AddCommSemigroup R
inst_5 : Sub R
inst_6 : ContinuousSub R
inst_7 : OrderedSub R
inst_8 : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
⊢ liminf (fun (i : ι) ↦ c - f i) F = c - limsup f F

Tactic:
(Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt bdd_above cobdd).symm

Premises used: Filter.liminf, Set.Mem, Antitone.map_limsSup_of_continuousAt, Filter.map, setOf, Filter.limsup, tsub_le_tsub_left, Continuous.continuousAt, Set.preimage, Eq.symm, continuous_sub_left
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : AddCommSemigroup R
inst_5 : Sub R
inst_6 : ContinuousSub R
inst_7 : OrderedSub R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
⊢ liminf (fun (i : ι) ↦ f i - c) F = liminf f F - c

Tactic:
(Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt cobdd bdd_below).symm

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Continuous.continuousAt, Set.preimage, Monotone.map_limsInf_of_continuousAt, tsub_le_tsub_right, Eq.symm, continuous_sub_right
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
apply : mulTSupport (f ⊔ g) ⊆ mulTSupport f ∪ mulTSupport g
⊢ HasCompactMulSupport (f ⊔ g)

Tactic:
apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)

Premises used: isClosed_mulTSupport, IsCompact.of_isClosed_subset, IsCompact.union
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
rw : closure (Function.mulSupport (f ⊔ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)
⊢ mulTSupport (f ⊔ g) ⊆ mulTSupport f ∪ mulTSupport g

Tactic:
rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]

Premises used: closure_union, mulTSupport
-- Module: Mathlib.Topology.Algebra.Order.Support
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeSup M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
h : Function.mulSupport (f ⊔ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g
⊢ closure (Function.mulSupport (f ⊔ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)

Tactic:
apply closure_mono

Premises used: closure_mono