awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
⊢ liminf u f + liminf v f ≤ liminf (u + v) f
have refine : ∀ (a : EReal) (a_u : a < liminf u f) (b : EReal) (b_v : b < liminf v f) (c : EReal) (c_ab : c < a + b),
  ∀ᶠ (a : α) in f, c < (u + v) a
Tactic: refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
⊢ ∀ᶠ (a : α) in f, c < (u + v) a
have h : ∀ (x : α) (a_x : a < u x) (b_x : b < v x), c < (u + v) x
Tactic: filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
⊢ limsup (u + v) f ≤ limsup u f + limsup v f
have refine : ∀ (a : EReal) (a_u : a > limsup u f) (b : EReal) (b_v : b > limsup v f) (c : EReal) (c_ab : c > a + b),
  ∀ᶠ (a : α) in f, (u + v) a < c
Tactic: refine le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
⊢ ∀ᶠ (a : α) in f, (u + v) a < c
have h₁ : ∀ (x : α) (a_x : u x < a) (b_x : v x < b), (u + v) x < c
Tactic: filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup (u + v) f = ⊥
have apply : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
Tactic: apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
apply : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
⊢ limsup (u + v) f = ⊥
have apply₁ : limsup u f + limsup v f ≤ ⊥
Tactic: apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
have rw : Ne (α := EReal) ⊥ ⊤ ∨ limsup v f ≠ ⊥
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥
have rw : ⊥ + limsup v f ≤ ⊥
Tactic: rw [h, bot_add]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
rw : ⊥ + limsup v f ≤ ⊥
⊢ limsup u f + limsup v f ≤ ⊥
have rw₁ : LE.le (α := EReal) ⊥ ⊥
Tactic: rw [h, bot_add]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
⊢ limsup (u + v) f ≤ a + b
have inl : ∀ (hb : limsup v f ≤ ⊤), limsup (u + v) f ≤ a + ⊤
Tactic: rcases eq_top_or_lt_top b with rfl | h
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
inl : ∀ (hb : limsup v f ≤ ⊤), limsup (u + v) f ≤ a + ⊤
⊢ limsup (u + v) f ≤ a + b
have inr : ∀ (h : b < ⊤), limsup (u + v) f ≤ a + b
Tactic: rcases eq_top_or_lt_top b with rfl | h
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ a + ⊤
have inl : limsup (u + v) f ≤ ⊤
Tactic: rw [add_top_of_ne_bot ha.ne_bot]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ liminf (u + v) f = ⊤
have apply : ⊤ ≤ liminf u f + liminf v f
Tactic: apply top_le_iff.1 (le_trans _ le_liminf_add)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ liminf u f + liminf v f
have rw : ⊤ ≤ ⊤ + liminf v f
Tactic: rw [h, top_add_of_ne_bot h']
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
rw : ⊤ ≤ ⊤ + liminf v f
⊢ ⊤ ≤ liminf u f + liminf v f
have rw₁ : LE.le (α := EReal) ⊤ ⊤
Tactic: rw [h, top_add_of_ne_bot h']
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ limsup (fun (x : α) ↦ c * u x) f = c * limsup u f
have inl : ∀ (h₁ : LE.le (α := EReal) 0 0) (h₂ : Ne (α := EReal) 0 ⊤), limsup (fun (x : α) ↦ 0 * u x) f = 0 * limsup u f
Tactic: obtain rfl | h₃ := h₁.eq_or_lt
Cleared hypotheses: c, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
inl : ∀ (h₁ : LE.le (α := EReal) 0 0) (h₂ : Ne (α := EReal) 0 ⊤), limsup (fun (x : α) ↦ 0 * u x) f = 0 * limsup u f
⊢ limsup (fun (x : α) ↦ c * u x) f = c * limsup u f
have inr : ∀ (h₃ : 0 < c), limsup (fun (x : α) ↦ c * u x) f = c * limsup u f
Tactic: obtain rfl | h₃ := h₁.eq_or_lt
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun (x : α) ↦ c * u x) f = c * limsup u f
have inr : limsup (fun (x : α) ↦ u x * c) f = limsup u f * c
Tactic: simp_rw [EReal.mul_comm (x := c)]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun (x : α) ↦ u x * c) f = limsup u f * c
have inr : limsup (fun (x : α) ↦ u x * c) f ≤ limsup u f * c
Tactic: apply eq_of_le_of_ge
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
inr : limsup (fun (x : α) ↦ u x * c) f ≤ limsup u f * c
⊢ limsup (fun (x : α) ↦ u x * c) f = limsup u f * c
have inr₁ : limsup u f * c ≤ limsup (fun (x : α) ↦ u x * c) f
Tactic: apply eq_of_le_of_ge
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun (x : α) ↦ u x * c) f ≤ limsup u f * c
have inr : ∀ y > limsup u f * c, ∀ᶠ (a : α) in f, u a * c < y
Tactic: rw [limsup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup u f * c ≤ limsup (fun (x : α) ↦ u x * c) f
have inr : ∀ y < limsup u f * c, ∃ᶠ (a : α) in f, y < u a * c
Tactic: rw [le_limsup_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have inl : ∀ (hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x) (hv : 0 ≤ᶠ[⊥] v), limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
Tactic: rcases f.eq_or_neBot with rfl | _
Cleared hypotheses: f, hu, hv
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
inl : ∀ (hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x) (hv : 0 ≤ᶠ[⊥] v), limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have inr : f.NeBot → limsup u f * liminf v f ≤ limsup (u * v) f
Tactic: rcases f.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
have inl : ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
Tactic: rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
inl : ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
have inl₁ : ⊥ * liminf v ⊥ ≤ ⊥
Tactic: rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
inl : ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
inl₁ : ⊥ * liminf v ⊥ ≤ ⊥
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
have inl₂ : HMul.hMul (α := EReal) ⊥ ⊤ ≤ ⊥
Tactic: rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
inl : ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
inl₁ : ⊥ * liminf v ⊥ ≤ ⊥
inl₂ : HMul.hMul (α := EReal) ⊥ ⊤ ≤ ⊥
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
have inl₃ : LE.le (α := EReal) ⊥ ⊥
Tactic: rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have u0 : 0 ≤ limsup u f
Tactic: have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have uv0 : 0 ≤ limsup (u * v) f
Tactic: have uv0 : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_le <| (hu.and_eventually hv).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have inr : ∀ (a : EReal) (ha : a ∈ Ioo 0 (limsup u f)) (b : EReal) (hb : b ∈ Ioo 0 (liminf v f)) (c : EReal) (c_ab : c < a * b),
  ∃ᶠ (a : α) in f, c < (u * v) a
Tactic: refine mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∃ᶠ (a : α) in f, c < (u * v) a
have inr : ∀ (x : α), a < u x ∧ b < v x ∧ 0 x ≤ v x → ∀ (xa : a < u x) (xb : b < v x) (vx : 0 x ≤ v x), c < (u * v) x
Tactic: refine (((frequently_lt_of_lt_limsup) (mem_Ioo.1 ha).2).and_eventually
    <| (eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2).and
    <| hv).mono fun x ⟨xa, ⟨xb, vx⟩⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have inl : ∀ (hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x) (hv : 0 ≤ᶠ[⊥] v) (h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤)
  (h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0), limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥
Tactic: rcases f.eq_or_neBot with rfl | _
Cleared hypotheses: f, hu, hv, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
inl :
  ∀ (hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x) (hv : 0 ≤ᶠ[⊥] v) (h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤)
    (h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0), limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have inr : f.NeBot → limsup (u * v) f ≤ limsup u f * limsup v f
Tactic: rcases f.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥
have inl : ⊥ ≤ limsup u ⊥ * limsup v ⊥
Tactic: rw [limsup_bot]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h : f.NeBot
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have u_0 : 0 ≤ limsup u f
Tactic: have u_0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h : f.NeBot
u_0 : 0 ≤ limsup u f
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have h₃ : 0 < limsup u f ∨ limsup v f ≠ ⊤
Tactic: replace h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤ := h₁.imp_left fun h ↦ lt_of_le_of_ne u_0 h.symm
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have h₃ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
Tactic: replace h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f :=
    h₂.imp_right fun h ↦ lt_of_le_of_ne (le_limsup_of_frequently_le hv.frequently) h.symm
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have inr : ∀ (a : EReal) (a_u : a > limsup u f) (b : EReal) (b_v : b > limsup v f) (c : EReal) (c_ab : c > a * b),
  ∀ᶠ (a : α) in f, (u * v) a < c
Tactic: refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c
have h : ∀ (x : α) (x_a : u x < a) (x_b : v x < b) (v_0 : 0 x ≤ v x), (u * v) x < c
Tactic: filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, hv]
    with x x_a x_b v_0
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
⊢ (u * v) x < c
have apply : (u * v) x ≤ a * b
Tactic: apply lt_of_le_of_lt _ c_ab
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ a * b
have inl : ∀ (hux : u x < 0), (u * v) x ≤ a * b
Tactic: rcases lt_or_ge (u x) 0 with hux | hux
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
inl : ∀ (hux : u x < 0), (u * v) x ≤ a * b
⊢ (u * v) x ≤ a * b
have inr : ∀ (hux : 0 ≤ u x), (u * v) x ≤ a * b
Tactic: rcases lt_or_ge (u x) 0 with hux | hux
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
hux : u x < 0
⊢ (u * v) x ≤ a * b
have inl : 0 ≤ a * b
Tactic: apply (mul_nonpos_iff.2 (.inr ⟨hux.le, v_0⟩)).trans
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ liminf u f * liminf v f ≤ liminf (u * v) f
have apply : ∀ a' ∈ Ioo 0 (liminf u f), ∀ b' ∈ Ioo 0 (liminf v f), a' * b' ≤ liminf (fun (x : α) ↦ u x * v x) f
Tactic: apply mul_le_of_forall_lt_of_nonneg ((le_liminf_of_le) hu)
    <| (le_liminf_of_le) ((hu.and hv).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ ∀ a' ∈ Ioo 0 (liminf u f), ∀ b' ∈ Ioo 0 (liminf v f), a' * b' ≤ liminf (fun (x : α) ↦ u x * v x) f
have refine : ∀ (a : EReal) (ha : a ∈ Ioo 0 (liminf u f)) (b : EReal) (hb : b ∈ Ioo 0 (liminf v f)) (c : EReal) (c_ab : c < a * b),
  ∀ᶠ (a : α) in f, c < u a * v a
Tactic: refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < u a * v a
have h : ∀ (x : α) (xa : a < u x) (xb : b < v x), c < u x * v x
Tactic: filter_upwards [eventually_lt_of_lt_liminf (mem_Ioo.1 ha).2,
    eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2] with x xa xb
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
inst : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ 0 < limsup u f ∨ liminf v f ≠ ⊤
have refine : ∀ (h : limsup u f ≠ 0), 0 ≤ limsup u f
Tactic: refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
inst : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ liminf (u * v) f ≤ limsup u f * liminf v f
have h₃ : 0 < limsup u f ∨ liminf v f ≠ ⊤
Tactic: replace h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤ := by
    refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm
    exact le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
inst : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ 0 < liminf v f
have refine : ∀ (h : liminf v f ≠ 0), 0 ≤ liminf v f
Tactic: refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
inst : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
⊢ liminf (u * v) f ≤ limsup u f * liminf v f
have h₃ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
Tactic: replace h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f := by
    refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm
    exact le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
inst : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
⊢ liminf (u * v) f ≤ limsup u f * liminf v f
have refine : ∀ (a : EReal) (a_u : a > limsup u f) (b : EReal) (b_v : b > liminf v f) (c : EReal) (c_ab : c > a * b),
  ∃ᶠ (a : α) in f, (u * v) a < c
Tactic: refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
inst : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
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) b_v).and_eventually <| (eventually_lt_of_limsup_lt a_u).and
    <| hu.and hv).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))
have simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 + a.2
Tactic: simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 + a.2
have refine : ∀ (r : ℝ) (x : EReal × EReal) (h : (↑(r - (a - 1)) : EReal) < x.1 ∧ (↑(a - 1) : EReal) < x.2), (↑r : EReal) < x.1 + x.2
Tactic: refine fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
    (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊤)
have simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 + a.2
Tactic: simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 + a.2
have refine : ∀ (r : ℝ) (x : EReal × EReal) (h : (↑0 : EReal) < x.1 ∧ (↑r : EReal) < x.2), (↑r : EReal) < x.1 + x.2
Tactic: refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))
have simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, (↑a : EReal)), a.1 + a.2 < (↑x : EReal)
Tactic: simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]