awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
⊢ liminf u f * liminf v f ≤ liminf (u * v) f
have apply : ∀ a' ≥ 0, a' < liminf u f → ∀ b' ≥ 0, b' < liminf v f → a' * b' ≤ liminf (u * v) f
Tactic: apply mul_le_of_forall_lt_of_nonneg (le_liminf_of_le h₂.isCoboundedUnder_ge h₁)
    (le_liminf_of_le h ((h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
⊢ a * b ≤ liminf (u * v) f
have refine : ∀ (c : ℝ) (c_ab : c < a * b), ∀ᶠ (a : ι) in f, c < (u * v) a
Tactic: refine (le_liminf_iff h h').2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
⊢ ∀ᶠ (a : ι) in f, c < (u * v) a
have h₅ : ∀ (x : ι) (xa : a < u x) (xb : b < v x), c < (u * v) x
Tactic: filter_upwards [eventually_lt_of_lt_liminf au (isBoundedUnder_of_eventually_ge h₁),
    eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)] with x xa xb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
⊢ liminf (u * v) f ≤ limsup u f * liminf v f
have h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
Tactic: have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
⊢ liminf (u * v) f ≤ limsup u f * liminf v f
have h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
Tactic: have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
⊢ liminf (u * v) f ≤ limsup u f * liminf v f
have refine : ∀ (a : ℝ) (a_u : a > limsup u f) (b : ℝ) (b_v : b > liminf v f) (c : ℝ) (c_ab : c > a * b),
  ∃ᶠ (a : ι) in f, (u * v) a < c
Tactic: refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
⊢ ∃ᶠ (a : ι) in f, (u * v) a < c
have refine : ∀ (x : ι),
  v x < b ∧ u x < a ∧ 0 x ≤ u x ∧ 0 x ≤ v x →
    ∀ (x_v : v x < b) (x_u : u x < a) (u_0 : 0 x ≤ u x) (v_0 : 0 x ≤ v x), (u * v) x < c
Tactic: refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
    (h₁.and h₃))).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F
have 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 ⊥
Tactic: rcases F.eq_or_neBot with rfl | _
Cleared hypotheses: F, cobdd, bdd_below
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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 ⊥
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F
have inr : F.NeBot → limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F
Tactic: rcases F.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ c - f i) ⊥ = c - liminf f ⊥
have inl : sInf Set.univ = c - sSup Set.univ
Tactic: simp only [liminf, limsInf, limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ sInf Set.univ = c - sSup Set.univ
have cobdd₁ : ∃ (b : R), ∀ (a : R), b ≥ a
Tactic: simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
Cleared hypotheses: cobdd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ sInf Set.univ = c - sSup Set.univ
have inl : ∀ (x : R) (hx : ∀ (a : R), x ≥ a), sInf Set.univ = c - sSup Set.univ
Tactic: rcases cobdd with ⟨x, hx⟩
Cleared hypotheses: cobdd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have inl : BddBelow.{u_4} (α := R) Set.univ
Tactic: refine (csInf_le ?_ (Set.mem_univ _)).antisymm
      (tsub_le_iff_tsub_le.1 (le_csSup ?_ (Set.mem_univ _)))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ sInf Set.univ = c - sSup Set.univ
have inl₁ : BddAbove.{u_4} (α := R) Set.univ
Tactic: refine (csInf_le ?_ (Set.mem_univ _)).antisymm
      (tsub_le_iff_tsub_le.1 (le_csSup ?_ (Set.mem_univ _)))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have inl : ∀ (y : R), Membership.mem (γ := Set R) Set.univ y → x - x ≤ y
Tactic: refine ⟨x - x, mem_lowerBounds.2 fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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 → x - x ≤ y
have inl : x - x ≤ y
Tactic: simp only [Set.mem_univ, true_implies]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have inl : ∀ (y : R), Membership.mem (γ := Set R) Set.univ y → y ≤ x
Tactic: refine ⟨x, mem_upperBounds.2 fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
have 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
Tactic: rcases F.eq_or_neBot with rfl | _
Cleared hypotheses: F, bdd_above, cobdd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
have inr : F.NeBot → limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
Tactic: rcases F.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have apply : BddBelow.{u_4} (α := R) Set.univ
Tactic: apply csInf_le _ (Set.mem_univ a)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ BddBelow.{u_4} (α := R) Set.univ
have cobdd₁ : ∃ (b : R), ∀ (a : R), b ≤ a
Tactic: simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
Cleared hypotheses: cobdd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ BddBelow.{u_4} (α := R) Set.univ
have rcases : ∀ (x : R) (hx : ∀ (a : R), x ≤ a), BddBelow.{u_4} (α := R) Set.univ
Tactic: rcases cobdd with ⟨x, hx⟩
Cleared hypotheses: cobdd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have refine : ∀ (y : R), Membership.mem (γ := Set R) Set.univ y → x ≤ y
Tactic: refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c
have this : ∀ {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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c
have inl : sInf Set.univ = sInf Set.univ - c
Tactic: simp only [limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
have apply : Monotone (β := R) fun (x : R) ↦ x - c
Tactic: apply (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) _ _).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
have apply₁ : ContinuousAt (Y := R) (fun (x : R) ↦ x - c) (map f F).limsSup
Tactic: apply (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) _ _).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Support (goal)
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
⊢ HasCompactMulSupport (f ⊔ g)
have apply : mulTSupport (f ⊔ g) ⊆ mulTSupport f ∪ mulTSupport g
Tactic: apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Support (goal)
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
⊢ mulTSupport (f ⊔ g) ⊆ mulTSupport f ∪ mulTSupport g
have rw : closure (Function.mulSupport (f ⊔ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)
Tactic: rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Support (goal)
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
⊢ closure (Function.mulSupport (f ⊔ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)
have h : Function.mulSupport (f ⊔ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Support (goal)
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ HasCompactMulSupport (f ⊓ g)
have apply : mulTSupport (f ⊓ g) ⊆ mulTSupport f ∪ mulTSupport g
Tactic: apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Support (goal)
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ mulTSupport (f ⊓ g) ⊆ mulTSupport f ∪ mulTSupport g
have rw : closure (Function.mulSupport (f ⊓ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)
Tactic: rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Support (goal)
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : One M
inst_2 : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ closure (Function.mulSupport (f ⊓ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)
have h : Function.mulSupport (f ⊓ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)
have rw : y ∈ (y / x) • closure s
Tactic: rw [closure_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)
have rw : y ∈ (y / x) • closure s
Tactic: rw [closure_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (↑(upperClosure s) : Set α)
have rw : IsOpen (s * (↑(upperClosure 1) : Set α))
Tactic: rw [← mul_one s, ← mul_upperClosure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : Preorder α
inst_3 : IsOrderedMonoid α
inst_4 : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (↑(lowerClosure s) : Set α)
have rw : IsOpen (s * (↑(lowerClosure 1) : Set α))
Tactic: rw [← mul_one s, ← mul_lowerClosure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsUpperSet (interior s)
have rw : IsLowerSet (closure sᶜ)
Tactic: rw [← isLowerSet_compl, ← closure_compl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
⊢ (interior s).OrdConnected
have rw : (interior (↑(upperClosure s) : Set α) ∩ interior (↑(lowerClosure s) : Set α)).OrdConnected
Tactic: rw [← h.upperClosure_inter_lowerClosure, interior_inter]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous (Y := R) fun (x : R) ↦ eval₂ f x p
have simp : Continuous (Y := R) fun (x : R) ↦ p.sum fun (e : ℕ) (a : S) ↦ HMul.hMul (α := R) ((f : (a : S) → R) a : R) (x ^ e)
Tactic: simp only [eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Polynomial (goal)
Goal:
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst : Semiring R
inst_1 : Ring S
inst_2 : Field k
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst_5 : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
have revert : ∀ (hf : Ne.{u_2 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)),
  Tendsto.{u_4, u_3} (β := k) (fun (x : α) ↦ abv (eval₂ f (z x) p)) l atTop
Tactic: revert hf
Cleared hypotheses: hf