awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
⊢ t.truncateToReal x = x.toReal
have x_lt_top : x < ∞
Tactic: have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
⊢ t.truncateToReal x = x.toReal
have obs : min t x ≠ ∞
Tactic: have obs : min t x ≠ ∞ := by
    simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ (min t x).toReal ≤ t.toReal
have h : min t x ≤ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ (min t x).toReal ≤ (min t y).toReal
have hb : min t y ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ Continuous t.truncateToReal
have apply : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (min t x)
Tactic: apply continuousOn_toReal.comp_continuous (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
have inl : limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c
Tactic: rcases F.eq_or_neBot with rfl | _
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
inl : 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.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F
have inl : limsup (fun (i : ι) ↦ c - f i) ⊥ = c - liminf f ⊥
Tactic: rcases F.eq_or_neBot with rfl | _
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
inl : 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.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
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 refine : ∀ (a : ℝ≥0∞) (a_u : a > limsup u f) (b : ℝ≥0∞) (b_v : b > limsup v f) (c : ℝ≥0∞) (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.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
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.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
⊢ liminf u f * liminf v f ≤ liminf (u * v) f
have refine : ∀ (a : ℝ≥0∞) (a_u : a < liminf u f) (b : ℝ≥0∞) (b_v : b < liminf v f) (c : ℝ≥0∞) (c_ab : c < a * b),
  ∀ᶠ (a : ι) in f, c < (u * v) a
Tactic: refine mul_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.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
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.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ liminf u f ≤ b
have apply : ∀ (b_1 : ℝ≥0∞), (∀ᶠ (n : ι) in f, b_1 ≤ u n) → b_1 ≤ b
Tactic: apply liminf_le_of_le ⟨0, by simp⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in f, y ≤ u n
⊢ y ≤ b
have obtain : ∀ (i : ι) (hi : y ≤ u i ∧ u i ≤ b), y ≤ b
Tactic: obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ liminf (fun (i : ι) ↦ (u i).toReal) f = (liminf u f).toReal
have liminf_le : liminf u f ≤ b
Tactic: have liminf_le : f.liminf u ≤ b := by
    apply liminf_le_of_le ⟨0, by simp⟩
    intro y h
    obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
    exact hi.1.trans hi.2
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
have h : ∀ (i : ι) (i_le_b : u i ≤ b), (u i).toReal = b.truncateToReal (u i)
Tactic: filter_upwards [le_b] with i i_le_b
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
⊢ liminf (fun (i : ι) ↦ (u i).toReal) f = (liminf u f).toReal
have aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
Tactic: have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ (liminf u f).toReal = b.truncateToReal (liminf u f)
have rw : (liminf u f).toReal = (liminf u f).toReal
Tactic: rw [truncateToReal_eq_toReal b_ne_top liminf_le]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ liminf (fun (i : ι) ↦ (u i).toReal) f = (liminf u f).toReal
have aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
Tactic: have aux' : (f.liminf u).toReal = ENNReal.truncateToReal b (f.liminf u) := by
    rw [truncateToReal_eq_toReal b_ne_top liminf_le]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ liminf (fun (i : ι) ↦ (u i).toReal) f = (liminf u f).toReal
have simp_rw : liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)
Tactic: simp_rw [liminf_congr aux, aux']
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)
have key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
Tactic: have key := Monotone.map_liminf_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
          (continuous_truncateToReal b_ne_top).continuousAt
          (IsBoundedUnder.isCoboundedUnder_ge ⟨b, by simpa only [eventually_map] using le_b⟩)
          ⟨0, Eventually.of_forall (by simp)⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)
have rw : liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = liminf (b.truncateToReal ∘ u) f
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
have h : ∀ (i : ι) (i_le_b : u i ≤ b), (u i).toReal = b.truncateToReal (u i)
Tactic: filter_upwards [le_b] with i i_le_b
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ limsup (fun (i : ι) ↦ (u i).toReal) f = (limsup u f).toReal
have aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
Tactic: have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ (limsup u f).toReal = b.truncateToReal (limsup u f)
have rw : (limsup u f).toReal = (limsup u f).toReal
Tactic: rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ limsup (fun (i : ι) ↦ (u i).toReal) f = (limsup u f).toReal
have aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
Tactic: have aux' : (f.limsup u).toReal = ENNReal.truncateToReal b (f.limsup u) := by
    rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ limsup (fun (i : ι) ↦ (u i).toReal) f = (limsup u f).toReal
have simp_rw : limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)
Tactic: simp_rw [limsup_congr aux, aux']
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)
have key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
Tactic: have key := Monotone.map_limsup_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
          (continuous_truncateToReal b_ne_top).continuousAt
          ⟨b, by simpa only [eventually_map] using le_b⟩
          (IsBoundedUnder.isCoboundedUnder_le ⟨0, Eventually.of_forall (by simp)⟩)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
⊢ limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)
have rw : limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = limsup (b.truncateToReal ∘ u) f
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ (↑(limsup u f) : ℝ≥0∞) = limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
have refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑(limsup u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
Tactic: refine eq_of_forall_nnreal_le_iff fun r ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ (↑(limsup u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
have rw : (∀ y < r, ∃ᶠ (a : ι) in f, y < u a) ↔ ∀ y < (↑r : ℝ≥0∞), ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ≥0∞)
Tactic: rw [coe_le_coe, le_limsup_iff, le_limsup_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
⊢ (↑(liminf u f) : ℝ≥0∞) = liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
have refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑(liminf u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
Tactic: refine eq_of_forall_nnreal_le_iff fun r ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ (↑(liminf u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
have rw : (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ∀ y < (↑r : ℝ≥0∞), ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ≥0∞)
Tactic: rw [coe_le_coe, le_liminf_iff, le_liminf_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ liminf (f + g) u = liminf f u
have refine : liminf (f + g) u ≤ liminf f u
Tactic: refine le_antisymm ?_ <| liminf_le_liminf <| .of_forall <| by simp
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ liminf (f + g) u ≤ liminf f u
have refine : ∀ (b : ℝ≥0∞) (hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n), b ≤ liminf f u
Tactic: refine liminf_le_of_le (by isBoundedDefault) fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
⊢ b ≤ liminf f u
have rw : ∀ y < b, ∀ᶠ (a : ι) in u, y ≤ f a
Tactic: rw [Filter.le_liminf_iff']
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
⊢ ∀ᶠ (a_1 : ι) in u, a ≤ f a_1
have h : ∀ (i : ι) (hfg : b ≤ (f + g) i) (hg : g i ≤ min (b - a) 1), a ≤ f i
Tactic: filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| lt_min (tsub_pos_of_lt hab) one_pos]
    with i hfg hg
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ liminf (f + g) u = liminf g u
have rw : liminf (g + f) u = liminf g u
Tactic: rw [add_comm, liminf_add_of_right_tendsto_zero hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
rw : liminf (g + f) u = liminf g u
⊢ liminf (f + g) u = liminf g u
have rw₁ : liminf g u = liminf g u
Tactic: rw [add_comm, liminf_add_of_right_tendsto_zero hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ limsup (f + g) u = limsup f u
have refine : limsup (f + g) u ≤ limsup f u
Tactic: refine le_antisymm ?_ <| limsup_le_limsup <| .of_forall <| by simp
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ limsup (f + g) u ≤ limsup f u
have refine : ∀ (b : ℝ≥0∞) (hb : ∀ᶠ (n : ι) in u, f n ≤ b), limsup (f + g) u ≤ b
Tactic: refine le_limsup_of_le (by isBoundedDefault) fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
⊢ limsup (f + g) u ≤ b
have rw : ∀ y > b, ∀ᶠ (a : ι) in u, (f + g) a ≤ y
Tactic: rw [Filter.limsup_le_iff']
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
⊢ ∀ᶠ (a_1 : ι) in u, (f + g) a_1 ≤ a
have h : ∀ (i : ι) (hf : f i ≤ b) (hg : g i ≤ a - b), (f + g) i ≤ a
Tactic: filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| tsub_pos_of_lt hba] with i hf hg
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg_1 : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ (f + g) i ≤ a
have calc : f i + g i ≤ b + g i
Tactic: calc f i + g i
    _ ≤ b + g i := by gcongr
    _ ≤ a := add_le_of_le_tsub_left_of_le hba.le hg
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ limsup (f + g) u = limsup g u
have rw : limsup (g + f) u = limsup g u
Tactic: rw [add_comm, limsup_add_of_right_tendsto_zero hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
rw : limsup (g + f) u = limsup g u
⊢ limsup (f + g) u = limsup g u
have rw₁ : limsup g u = limsup g u
Tactic: rw [add_comm, limsup_add_of_right_tendsto_zero hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
have this : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
  (hs.extend (s := s) f)
Tactic: have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)
⊢ IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
have apply : Continuous[instTopologicalSpaceProd, _] fun (b : α × α) ↦ (↑K : ℝ≥0∞) * edist b.1 b.2
Tactic: apply isClosed_le (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ LipschitzWith K (hs.extend (s := s) f)
have this : IsClosed[instTopologicalSpaceProd]
  {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
Tactic: have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
    apply isClosed_le (by fun_prop)
    exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
⊢ Dense.{u_4} (X := α × α)
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
have apply : s ×ˢ s ⊆ {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
Tactic: apply (hs.prod hs).mono
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
⊢ Membership.mem (γ := Set (α × α))
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2} (x, y)
have Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Tactic: have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
⊢ Membership.mem (γ := Set (α × α))
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2} (x, y)
have Ay : hs.extend (s := s) f y = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
Tactic: have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩