awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mp : (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) → ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
⊢ (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
have mpr : (∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y) → ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
Tactic: constructor
-- 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
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
⊢ ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < some x
have h₃ : ∀ (a : α) (ha : u a < (↑x : ℝ)), ENNReal.ofReal (u a) < some x
Tactic: filter_upwards [h x (by simpa using hx)] with a ha
-- 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
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
a : α
ha : u a < (↑x : ℝ)
⊢ ENNReal.ofReal (u a) < some x
have h₃ : ∀ (ha₀ : u a ≤ 0), ENNReal.ofReal (u a) < some x
Tactic: obtain ha₀ | ha₀ := le_total (u a) 0
-- 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
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
a : α
ha : u a < (↑x : ℝ)
h₃ : ∀ (ha₀ : u a ≤ 0), ENNReal.ofReal (u a) < some x
⊢ ENNReal.ofReal (u a) < some x
have h₄ : ∀ (ha₀ : 0 ≤ u a), ENNReal.ofReal (u a) < some x
Tactic: obtain ha₀ | ha₀ := le_total (u a) 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
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
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
⊢ ∀ᶠ (a : α) in f, u a < x
have this : 0 < x
Tactic: have : 0 < x := hx.trans_le' (by simp)
-- 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
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
this : 0 < x
⊢ ∀ᶠ (a : α) in f, u a < x
have h₃ : ∀ (a : α) (ha : ENNReal.ofReal (u a) < ENNReal.ofReal x), u a < x
Tactic: filter_upwards [h (.ofReal x) (by simpa [this] using hx)] with a ha
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
⊢ ENNReal.ofReal (limsup (fun (a : α) ↦ (u a).toReal) f) = limsup u f
have h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
Tactic: have h₁ : IsCoboundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) :=
    IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ by positivity
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
have refine : ∀ᶠ (x : α) in f, (u x).toReal ≤ (↑C : ℝ)
Tactic: refine isBoundedUnder_of_eventually_le (a := C) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ ∀ᶠ (x : α) in f, (u x).toReal ≤ (↑C : ℝ)
have h : ∀ (a : α) (ha : u a ≤ (↑C : ℝ≥0∞)), (u a).toReal ≤ (↑C : ℝ)
Tactic: filter_upwards [hf] with a ha
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ ENNReal.ofReal (limsup (fun (a : α) ↦ (u a).toReal) f) = limsup u f
have h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
Tactic: have h₂ : IsBoundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) := by
    refine isBoundedUnder_of_eventually_le (a := C) ?_
    filter_upwards [hf] with a ha
    exact ENNReal.toReal_le_coe_of_le_coe ha
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ ENNReal.ofReal (limsup (fun (a : α) ↦ (u a).toReal) f) = limsup u f
have refine : ∀ᶠ (a : α) in f, ENNReal.ofReal (u a).toReal = u a
Tactic: refine (ENNReal.ofReal_limsup h₁ h₂).trans (limsup_congr ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ ∀ᶠ (a : α) in f, ENNReal.ofReal (u a).toReal = u a
have h : ∀ (x : α) (hx : u x ≤ (↑C : ℝ≥0∞)), ENNReal.ofReal (u x).toReal = u x
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f
have inl : ∀ (h₁ : ∀ᶠ (a : α) in ⊥, u a ≠ ∞) (h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ⊥ fun (a : α) ↦ (u a).toReal),
  (limsup u ⊥).toReal = limsup (fun (a : α) ↦ (u a).toReal) ⊥
Tactic: obtain rfl | hf := f.eq_or_neBot
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
inl :
  ∀ (h₁ : ∀ᶠ (a : α) in ⊥, u a ≠ ∞) (h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ⊥ fun (a : α) ↦ (u a).toReal),
    (limsup u ⊥).toReal = limsup (fun (a : α) ↦ (u a).toReal) ⊥
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f
have inr : ∀ (hf : f.NeBot), (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f
Tactic: obtain rfl | hf := f.eq_or_neBot
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f
have this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
Tactic: have : IsCoboundedUnder (· ≤ ·) f fun a ↦ (u a).toReal := .of_frequently_ge (a := 0) (by simpa)
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f
have inr : ∀ (r : ℝ), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
Tactic: refine eq_of_forall_ge_iff fun r ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
have inr : ∀ (hr : r < 0), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
Tactic: obtain hr | hr := lt_or_ge r 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
inr : ∀ (hr : r < 0), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
have inr₁ : ∀ (hr : 0 ≤ r), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
Tactic: obtain hr | hr := lt_or_ge r 0
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
have inr : (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
Tactic: rw [← le_ofReal_iff_toReal_le _ hr, limsup_le_iff, limsup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
inr : (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
have rw : limsup u f ≠ ∞
Tactic: rw [← le_ofReal_iff_toReal_le _ hr, limsup_le_iff, limsup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
have inr : (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) → ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
inr : (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) → ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
⊢ (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
have inr₁ : (∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y) → ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y
x : ℝ
hx : x > r
⊢ ∀ᶠ (a : α) in f, (u a).toReal < x
have this₁ : 0 < x
Tactic: have : 0 < x := hx.trans_le' hr
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this_1 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y
x : ℝ
hx : x > r
this : 0 < x
⊢ ∀ᶠ (a : α) in f, (u a).toReal < x
have h₃ : ∀ (i : α) (hi : u i < ENNReal.ofReal x), (u i).toReal < x
Tactic: filter_upwards [h (.ofReal x) (by simpa [this] using hx)] with i hi
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
x : ℝ≥0
hx : some x > ENNReal.ofReal r
⊢ ∀ᶠ (a : α) in f, u a < some x
have h₃ : ∀ (i : α) (hi : u i ≠ ∞), (u i).toReal < (↑x : ℝ) → u i < some x
Tactic: filter_upwards [h₁, h x (by simpa [ofReal_lt_coe_iff hr] using hx)] with i hi
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ limsup u f ≠ ∞
have obtain : ∀ (x : ℝ) (hx : ∀ᶠ (x_1 : ℝ) in map (fun (a : α) ↦ (u a).toReal) f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x_1 x), limsup u f ≠ ∞
Tactic: obtain ⟨x, hx⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (x_1 : ℝ) in map (fun (a : α) ↦ (u a).toReal) f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x_1 x
⊢ limsup u f ≠ ∞
have hx₁ : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
Tactic: rw [eventually_map] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
⊢ 0 ≤ x
have obtain : ∀ (i : α) (hi : (u i).toReal ≤ x), 0 ≤ x
Tactic: obtain ⟨i, hi⟩ := hx.exists
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (hypothesis)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
⊢ limsup u f ≠ ∞
have hx₀ : 0 ≤ x
Tactic: have hx₀ : 0 ≤ x := by obtain ⟨i, hi⟩ := hx.exists; exact toReal_nonneg.trans hi
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ limsup u f ≠ ∞
have simp : ∃ (x : ℝ≥0∞) (_ : ∀ᶠ (a : α) in f, u a ≤ x), ¬x = ∞
Tactic: simp only [limsup, limsSup, eventually_map, ne_eq, sInf_eq_top, Set.mem_setOf_eq, not_forall]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ ∃ (x : ℝ≥0∞) (_ : ∀ᶠ (a : α) in f, u a ≤ x), ¬x = ∞
have refine : ∀ᶠ (a : α) in f, u a ≤ ENNReal.ofReal x
Tactic: refine ⟨.ofReal x, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ ∀ᶠ (a : α) in f, u a ≤ ENNReal.ofReal x
have h : ∀ (i : α) (hi : u i ≠ ∞), (u i).toReal ≤ x → u i ≤ ENNReal.ofReal x
Tactic: filter_upwards [h₁, hx] with i hi
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
c : β
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ c = 1 ∨ EventuallyConst s l
have inl : EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ 1) l ↔ Eq.{u_2 + 1} (α := β) 1 1 ∨ EventuallyConst s l
Tactic: rcases eq_or_ne c 1 with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
c : β
inl :
  EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ 1) l ↔
    Eq.{u_2 + 1} (α := β) 1 1 ∨ EventuallyConst s l
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ c = 1 ∨ EventuallyConst s l
have inr : ∀ (hc : c ≠ 1), EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ c = 1 ∨ EventuallyConst s l
Tactic: rcases eq_or_ne c 1 with rfl | hc
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
have rw : (∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
Tactic: rw [eventuallyConst_atTop]
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
f : ℕ → α
⊢ (∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
have refine_1 : ∀ (n : ℕ) (h : ∀ (j : ℕ), n ≤ j → f j = f n) (m : ℕ) (hm : n ≤ m), f (m + 1) = f m
Tactic: refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
f : ℕ → α
refine_1 : ∀ (n : ℕ) (h : ∀ (j : ℕ), n ≤ j → f j = f n) (m : ℕ) (hm : n ≤ m), f (m + 1) = f m
⊢ (∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
have refine_2 : ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m) (m : ℕ) (hm : n ≤ m), f m = f n
Tactic: refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
have refine_2 : f n = f n
Tactic: induction m, hm using Nat.le_induction with
    | base => rfl
    | succ m hm ihm => exact (h m hm).trans ihm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Filter.EventuallyConst (goal)
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
refine_2 : f n = f n
⊢ f m = f n
have refine_2₁ : ∀ (m : ℕ) (hm : n ≤ m) (ihm : f m = f n), f (m + 1) = f n
Tactic: induction m, hm using Nat.le_induction with
    | base => rfl
    | succ m hm ihm => exact (h m hm).trans ihm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
⊢ IsGLB {x : β | ∃ x_1 ∈ s, f x_1 = x} (f a)
have rw : ∀ (b : β), b ≤ f a ↔ Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ s, f x_1 = x}) b
Tactic: rw [isGLB_iff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ s, f x_1 = x}) b
have simp : b ≤ f a ↔ ∀ a ∈ s, b ≤ f a
Tactic: simp only [mem_lowerBounds, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
l : Filter α
a : α
β : Type u_1
inst : PartialOrder β
f : α → β
h₁ : IsMinFilter f l a
h₂ : IsMaxFilter f l a
⊢ f =ᶠ[l] fun (x : α) ↦ f a
have h : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f a ≤ f x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f a) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = (fun (x : α) ↦ f a) x) x} x}
          x}
    a_1
Tactic: filter_upwards [h₁, h₂] using by grind
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
l : Filter α
a : α
β : Type u_1
inst : PartialOrder β
f : α → β
h₁ : IsMinFilter f l a
h₂ : IsMaxFilter f l a
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f a ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f a) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = (fun (x : α) ↦ f a) x) x} x}
            x}
      a_1
⊢ f =ᶠ[l] fun (x : α) ↦ f a
have h₃ : ∀ (a_1 : α), f a ≤ f a_1 → f a_1 ≤ f a → f a_1 = f a
Tactic: filter_upwards [h₁, h₂] using by grind
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b