awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
have mp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) → ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
mp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) → ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
⊢ (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
have mpr : (∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)) → ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
⊢ (IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
have simp : (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) ↔
  ∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
        (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
Tactic: simp only [IsCoboundedUnder, IsCobounded, eventually_map, ← coe_le_coe, NNReal.forall,
    NNReal.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
⊢ (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
have mp : (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) →
  ∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
        (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
mp :
  (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) →
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
⊢ (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
have mpr : (∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
        (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
  ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
have simp : (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) ↔
  ∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
        (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
Tactic: simp only [IsCoboundedUnder, IsCobounded, eventually_map, ← coe_le_coe, NNReal.forall,
    NNReal.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
have mp : (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) →
  ∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
        (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
mp :
  (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) →
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
⊢ (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
have mpr : (∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
        (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)) →
  ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
⊢ ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a
have mpr : ∀ (x : ℝ) (hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x), b ≥ x
Tactic: refine ⟨b, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
⊢ b ≥ x
have mpr : ∀ (hx₀ : x ≤ 0), b ≥ x
Tactic: obtain hx₀ | hx₀ := le_total x 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
mpr : ∀ (hx₀ : x ≤ 0), b ≥ x
⊢ b ≥ x
have mpr₁ : ∀ (hx₀ : 0 ≤ x), b ≥ x
Tactic: obtain hx₀ | hx₀ := le_total x 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ≥0
hf : ¬IsBounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f
⊢ Eq (α := ℝ≥0) (sInf {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, n ≤ a}) ⊥
have h : Eq (α := Set ℝ≥0) {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, n ≤ a} ∅
Tactic: convert! sInf_empty
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ≥0
hf : ¬IsCobounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f
⊢ f.limsInf = 0
have rwa : Eq (α := ℝ≥0) (sSup {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}) 0
Tactic: rwa [limsInf, sSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ≥0
hf : ¬IsCobounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f
rwa : Eq (α := ℝ≥0) (sSup {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}) 0
⊢ f.limsInf = 0
have rwa₁ : Eq (α := ℝ≥0) 0 0
Tactic: rwa [limsInf, sSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ≥0
hf : ¬IsCobounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f
rwa : Eq (α := ℝ≥0) (sSup {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}) 0
rwa₁ : Eq (α := ℝ≥0) 0 0
⊢ f.limsInf = 0
have rwa₂ : ¬BddAbove (α := ℝ≥0) {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}
Tactic: rwa [limsInf, sSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
have pos : ∀ (hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u), liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
Tactic: by_cases hf : f.IsCoboundedUnder (· ≥ ·) u
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
pos :
  ∀ (hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u),
    liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
have neg : ∀ (hf : ¬IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u),
  liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
Tactic: by_cases hf : f.IsCoboundedUnder (· ≥ ·) u
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
have pos : ∀ (c : ℝ), c ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(liminf u f) : ℝ)
Tactic: refine eq_of_forall_le_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
⊢ c ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(liminf u f) : ℝ)
have pos : (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∀ᶠ (a : ι) in f, y < u a
Tactic: rw [← Real.toNNReal_le_iff_le_coe, le_liminf_iff (by simpa) ⟨0, by simp⟩, le_liminf_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∀ᶠ (a : ι) in f, y < u a
have pos : (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∀ᶠ (a : ι) in f, x < (↑(u a) : ℝ)
Tactic: simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∀ᶠ (a : ι) in f, x < (↑(u a) : ℝ)
have pos : ∀ (r : ℝ) (hr : r < c), (∀ᶠ (a : ι) in f, r < (↑(u a) : ℝ)) ↔ ∀ (a : 0 ≤ r), ∀ᶠ (a : ι) in f, r < (↑(u a) : ℝ)
Tactic: refine forall₂_congr fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
have inl : limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) ⊥ = (↑(limsup u ⊥) : ℝ)
Tactic: obtain rfl | hf := f.eq_or_neBot
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inl : limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) ⊥ = (↑(limsup u ⊥) : ℝ)
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
have inr : ∀ (hf : f.NeBot), limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
Tactic: obtain rfl | hf := f.eq_or_neBot
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
have pos : ∀ (hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u), limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
Tactic: by_cases hf : f.IsBoundedUnder (· ≤ ·) u
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
pos :
  ∀ (hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u), limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
have neg : ∀ (hf : ¬IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u), limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
Tactic: by_cases hf : f.IsBoundedUnder (· ≤ ·) u
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
have this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
Tactic: have : f.IsCoboundedUnder (· ≤ ·) u := by isBoundedDefault
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
have pos : ∀ (c : ℝ), c ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(limsup u f) : ℝ)
Tactic: refine eq_of_forall_le_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
⊢ c ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(limsup u f) : ℝ)
have pos : (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∃ᶠ (a : ι) in f, y < u a
Tactic: rw [← Real.toNNReal_le_iff_le_coe, le_limsup_iff (by simpa) (by simpa), le_limsup_iff ‹_›]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∃ᶠ (a : ι) in f, y < u a
have pos : (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∃ᶠ (a : ι) in f, x < (↑(u a) : ℝ)
Tactic: simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∃ᶠ (a : ι) in f, x < (↑(u a) : ℝ)
have pos : ∀ (r : ℝ) (hr : r < c), (∃ᶠ (a : ι) in f, r < (↑(u a) : ℝ)) ↔ ∀ (a : 0 ≤ r), ∃ᶠ (a : ι) in f, r < (↑(u a) : ℝ)
Tactic: refine forall₂_congr fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have pos : ∀ (ha₀ : a = 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
Tactic: by_cases ha₀ : a = 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
pos : ∀ (ha₀ : a = 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have neg : ∀ (ha₀ : ¬a = 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
Tactic: by_cases ha₀ : a = 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have pos : Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ ⊥) f) ⊥
Tactic: simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
have pos : ∀ (ha₀ : a = 0), liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
Tactic: by_cases ha₀ : a = 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
pos : ∀ (ha₀ : a = 0), liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
have neg : ∀ (ha₀ : ¬a = 0), liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
Tactic: by_cases ha₀ : a = 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
have pos : Eq (α := ℝ≥0∞) (liminf (fun (x : α) ↦ ⊥) f) ⊥
Tactic: simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have pos : ∀ (ha_top : a ≠ ∞), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
Tactic: by_cases! ha_top : a ≠ ⊤
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
pos : ∀ (ha_top : a ≠ ∞), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have neg : ∀ (ha_top : a = ∞), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
Tactic: by_cases! ha_top : a ≠ ⊤
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have pos : ∀ (hu : u =ᶠ[f] 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
Tactic: by_cases hu : u =ᶠ[f] 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
pos : ∀ (hu : u =ᶠ[f] 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have neg : ∀ (hu : ¬u =ᶠ[f] 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
Tactic: by_cases hu : u =ᶠ[f] 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have hau : f.EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ a * u x) 0
Tactic: have hau : (a * u ·) =ᶠ[f] 0 := hu.mono fun x hx => by simp [hx]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : f.EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ a * u x) 0
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have pos : ⊥ = a * ⊥
Tactic: simp only [limsup_congr hu, limsup_congr hau, Pi.zero_def, ← ENNReal.bot_eq_zero,
      limsup_const_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
⊢ ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
have hu₁ : ∃ᶠ (x : α) in f, ¬u x = 0 x
Tactic: rw [EventuallyEq, not_eventually] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have hu_mul : ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
Tactic: have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ := by
      rw [EventuallyEq, not_eventually] at hu
      exact hu.mono fun x hx => by simpa
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have h_top_le : Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ if u x = 0 then 0 else ∞) f) ∞
Tactic: have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
      eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
h_top_le : Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ if u x = 0 then 0 else ∞) f) ∞
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
have hfu : limsup u f ≠ 0
Tactic: have hfu : f.limsup u ≠ 0 := mt limsup_eq_bot.1 hu
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ limsup (u * v) f ≤ limsup (fun (x : α) ↦ limsup u f * v x) f
have refine : u * v ≤ᶠ[f] fun (x : α) ↦ limsup u f * v x
Tactic: refine limsup_le_limsup ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ u * v ≤ᶠ[f] fun (x : α) ↦ limsup u f * v x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ u y ≤ limsup u f) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (u * v) x ≤ (fun (x : α) ↦ limsup u f * v x) x) x} x}
    a
Tactic: filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ u y ≤ limsup u f) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (u * v) x ≤ (fun (x : α) ↦ limsup u f * v x) x) x} x}
      a
⊢ u * v ≤ᶠ[f] fun (x : α) ↦ limsup u f * v x
have h₁ : ∀ (a : α), u a ≤ limsup u f → (u * v) a ≤ limsup u f * v a
Tactic: filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Countable β
f : Filter α
inst_1 : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun (a' : α) ↦ u a' b) f
have rw : ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun (a' : α) ↦ u a' i) f
Tactic: rw [eventually_countable_forall]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
⊢ ENNReal.ofReal (limsup u f) = limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f
have refine : ∀ (r : ℝ≥0), ENNReal.ofReal (limsup u f) ≤ (↑r : ℝ≥0∞) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)
Tactic: refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ ENNReal.ofReal (limsup u f) ≤ (↑r : ℝ≥0∞) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)
have simp : limsup u f ≤ (↑r : ℝ) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)
Tactic: simp only [ofReal_le_coe]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ limsup u f ≤ (↑r : ℝ) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)
have rw : (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
Tactic: rw [limsup_le_iff, limsup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
have mp : (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) → ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
Tactic: constructor